diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9ea5c99a8a..92cf507ae2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,6 +13,35 @@ - in `normed_module.v`: + lemma `limit_point_infinite_setP` +- in `measurable_structure.v`: + + lemma `dynkin_induction`` + +- in `lebesgue_integral_fubini.v`: + + definition `product_subprobability` + + lemma `product_subprobability_setC` + +- new file `lebesgue_integral_theory/giry.v` + + definition `measure_eq` + + definition `giry` + + definition `giry_ev` + + definition `giry_measurable` + + definition `preimg_giry_ev` + + definition `giry_display` + + lemma `measurable_giry_ev` + + definition `giry_int` + + lemmas `measurable_giry_int`, `measurable_giry_codensity` + + definition `giry_map` + + lemmas `measurable_giry_map`, `giry_int_map`, `giry_map_dirac` + + definition `giry_ret` + + lemmas `measurable_giry_ret`, `giry_int_ret` + + definition `giry_join` + + lemmas `measurable_giry_join`, `sintegral_giry_join`, `giry_int_join` + + definition `giry_bind` + + lemmas `measurable_giry_bind`, `giry_int_bind` + + lemmas `giry_joinA`, `giry_join_id1`, `giry_join_id2`, `giry_map_zero` + + definition `giry_prod` + + lemmas `measurable_giry_prod`, `giry_int_prod1`, `giry_int_prod2` + ### Changed ### Renamed diff --git a/_CoqProject b/_CoqProject index 4a35dbab15..ccb3905b52 100644 --- a/_CoqProject +++ b/_CoqProject @@ -119,6 +119,7 @@ theories/lebesgue_integral_theory/lebesgue_Rintegral.v theories/lebesgue_integral_theory/lebesgue_integral_fubini.v theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v theories/lebesgue_integral_theory/lebesgue_integral.v +theories/lebesgue_integral_theory/giry.v theories/ftc.v theories/hoelder.v diff --git a/theories/Make b/theories/Make index 98c1b98895..d67f6b5447 100644 --- a/theories/Make +++ b/theories/Make @@ -86,6 +86,7 @@ lebesgue_integral_theory/lebesgue_Rintegral.v lebesgue_integral_theory/lebesgue_integral_fubini.v lebesgue_integral_theory/lebesgue_integral_differentiation.v lebesgue_integral_theory/lebesgue_integral.v +lebesgue_integral_theory/giry.v ftc.v hoelder.v diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v new file mode 100644 index 0000000000..ead9220485 --- /dev/null +++ b/theories/lebesgue_integral_theory/giry.v @@ -0,0 +1,467 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra boolp classical_sets. +From mathcomp Require Import fsbigop functions reals topology separation_axioms. +From mathcomp Require Import ereal sequences numfun measure measurable_realfun. +From mathcomp Require Import lebesgue_measure lebesgue_integral. + +(**md**************************************************************************) +(* # The Giry monad *) +(* *) +(* ``` *) +(* m1 ≡μ m2 == m1 S = m2 S for any measurable set S *) +(* giry T R == the type of subprobability measures over T *) +(* giry_ev P A == the evaluation map `giryM T R -> [0, 1]` *) +(* preimg_giry_ev A == preimage of the sigma-algebra of extended real numbers *) +(* via the function giry_ev ^~ A *) +(* giry_measurable == the sigma-algebra generated by the countable unions of *) +(* preimg_giry_ev *) +(* giry_display == display of giry_measurable *) +(* giry_int mu f := \int[mu]_x f x *) +(* giry_map mf == the map of type giry T1 R -> giry T2 R *) +(* where mf is a proof that f : T1 -> T2 is measurable *) +(* giry_ret x == the unit of the Giry monad, i.e., \d_x *) +(* @giry_join _ T R == the multiplication of the Giry monad *) +(* type : giry (giry T R) R -> giry T R *) +(* giry_bind mu mf == the bind with mu : giry T1 R and f : T1 -> giry T2 R *) +(* giry_prod == product of type *) +(* giry T1 R * giry T2 R -> giry (T1 * T2) R *) +(* ``` *) +(* *) +(******************************************************************************) + +Reserved Notation "m >>= f" (at level 49). + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. + +Definition measure_eq {d} {T : measurableType d} {R : realType} : + measure T R -> measure T R -> Prop := + fun m1 m2 => forall S : set T, measurable S -> m1 S = m2 S. +Notation "x ≡μ y" := (measure_eq x y) (at level 70). + +Global Hint Extern 0 (_ ≡μ _) => reflexivity : core. + +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. + +Section giry_def. +Context d (T : measurableType d) (R : realType). + +Definition giry : Type := @subprobability d T R. + +HB.instance Definition _ := gen_eqMixin giry. +HB.instance Definition _ := gen_choiceMixin giry. +HB.instance Definition _ := isPointed.Build giry mzero. + +Definition giry_ev (mu : giry) (A : set T) := mu A. + +Definition preimg_giry_ev (A : set T) : set_system giry := + preimage_set_system [set: giry] (giry_ev ^~ A) measurable. + +Definition giry_measurable := <>. + +Let giry_measurable0 : giry_measurable set0. +Proof. exact: sigma_algebra0. Qed. + +Let giry_measurableC (U : set giry) : + giry_measurable U -> giry_measurable (~` U). +Proof. exact: sigma_algebraC. Qed. + +Let giry_measurableU (F : (set giry)^nat) : + (forall i, giry_measurable (F i)) -> giry_measurable (\bigcup_i F i). +Proof. exact: sigma_algebra_bigcup. Qed. + +Definition giry_display : measure_display. +Proof. by constructor. Qed. + +HB.instance Definition _ := + @isMeasurable.Build giry_display giry giry_measurable + giry_measurable0 giry_measurableC giry_measurableU. + +Lemma measurable_giry_ev (A : set T) : measurable A -> + measurable_fun [set: giry] (giry_ev ^~ A). +Proof. +move=> mS. +apply: (@measurability giry_display _ giry _ setT (giry_ev ^~ A) measurable). + by rewrite smallest_id//; exact: sigma_algebra_measurable. +apply: subset_trans; last exact: sub_gen_smallest. +exact: (bigcup_sup mS). +Qed. + +End giry_def. +Arguments giry_ev {d T R} mu A. + +Section giry_integral. +Context d (T : measurableType d) (R : realType). + +Definition giry_int (mu : giry T R) (f : T -> \bar R) := \int[mu]_x f x. + +Import HBNNSimple. + +(**md The idea is to reconstruct f from simple functions, then use measurability + of giry_ev. Reference: Tom Avery. Codensity and the Giry monad. + https://arxiv.org/pdf/1410.4432. + *) +Lemma measurable_giry_int (f : T -> \bar R) : + measurable_fun [set: T] f -> (forall x, 0 <= f x) -> + measurable_fun [set: giry T R] (giry_int ^~ f). +Proof. +move=> mf h0. +pose g := nnsfun_approx measurableT mf. +pose Eg := fun n => EFin \o g n. +pose intEg := fun n mu => giry_int mu (Eg n). +have mintgE n : measurable_fun [set: giry T R] (intEg n). + rewrite /intEg /giry_int/=. + under eq_fun do rewrite integralT_nnsfun sintegralE. + apply: emeasurable_fsum => //= r. + by apply: measurable_funeM => //=; exact: measurable_giry_ev. +apply: (emeasurable_fun_cvg _ (giry_int ^~ f) mintgE) => mu _. +rewrite (_ : giry_int mu f = \int[mu]_x limn (Eg ^~ x)). + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n x _; rewrite lee_fin. + - by move=> t _ n m nm; apply/lefP/nd_nnsfun_approx. +apply: eq_integral => t _. +by apply/esym/cvg_lim => //; exact/cvg_nnsfun_approx. +Qed. + +End giry_integral. +Arguments giry_int {d T R} mu f. + +Section measurable_giry_codensity. +Context d1 {T1 : measurableType d1}. + +Lemma measurable_giry_codensity d2 {T2 : measurableType d2} {R : realType} + (D : set T1) (f : T1 -> giry T2 R) : + measurable D -> + (forall B, measurable B -> measurable_fun D (f ^~ B)) -> + measurable_fun D f. +Proof. +move=> mD mf. +pose G : set_system (giry T2 R) := \bigcup_(B in measurable) preimg_giry_ev B. +apply: (measurability G) => //= _ [_ [C mC [Z mZ] <-] <-]. +by rewrite setTI; exact: mf. +Qed. + +End measurable_giry_codensity. + +Section giry_map. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType}. +Variables (f : T1 -> T2) (mf : measurable_fun [set: T1] f) (mu1 : giry T1 R). + +Let map := pushforward mu1 f. + +Let map0 : map set0 = 0. Proof. exact: measure0. Qed. + +Let map_ge0 A : 0 <= map A. Proof. exact: measure_ge0. Qed. + +Let map_sigma_additive : semi_sigma_additive map. +Proof. exact: measure_semi_sigma_additive. Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ map + map0 map_ge0 map_sigma_additive. + +(* used to work before the change of definition of pushforward +HB.instance Definition _ := Measure.on gMap_ev. +the change of definition was maybe not a good idea... +https://github.com/math-comp/analysis/pull/1661 +*) + +Let map_setT : map [set: T2] <= 1. +Proof. by rewrite /map /pushforward /= sprobability_setT. Qed. + +HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ map map_setT. + +Definition giry_map : giry T2 R := map. + +End giry_map. + +Section giry_map_lemmas. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Variable f : T1 -> T2. +Hypothesis mf : measurable_fun [set: T1] f. + +Lemma measurable_giry_map : measurable_fun [set: giry T1 R] (giry_map mf). +Proof. +rewrite /giry_map. +apply: measurable_giry_codensity => // B mB. +apply: measurable_giry_ev. +by rewrite -(setTI (f @^-1` B)); exact: mf. +Qed. + +Lemma giry_int_map (mu : giry T1 R) (h : T2 -> \bar R) : + measurable_fun [set: T2] h -> (forall x, 0 <= h x) -> + giry_int (giry_map mf mu) h = giry_int mu (h \o f). +Proof. by move=> mh h0; exact: ge0_integral_pushforward. Qed. + +Lemma giry_map_dirac (mu1 : giry T1 R) (B : set T2) : measurable B -> + giry_map mf mu1 B = \int[mu1]_x (\d_(f x))%R B. +Proof. +move=> mB. +rewrite -[in LHS](setIT B) -[LHS]integral_indic// [LHS]giry_int_map//. + exact/measurable_EFinP/measurable_indic. +by move=> ?; rewrite lee_fin. +Qed. + +End giry_map_lemmas. + +Section giry_ret. +Context {d} {T : measurableType d} {R : realType}. + +Definition giry_ret (x : T) : giry T R := (\d_x)%R. + +Lemma measurable_giry_ret : measurable_fun [set: T] giry_ret. +Proof. +by apply: measurable_giry_codensity => //; exact: measurable_fun_dirac. +Qed. + +Lemma giry_int_ret (x : T) (f : T -> \bar R) : measurable_fun [set: T] f -> + giry_int (giry_ret x) f = f x. +Proof. +by move=> mf; rewrite /giry_int /giry_ret integral_dirac// diracT mul1e. +Qed. + +End giry_ret. + +Section giry_join. +Context {d} {T : measurableType d} {R : realType}. +Variable M : giry (giry T R) R. + +Let join A := giry_int M (giry_ev ^~ A). + +Let join0 : join set0 = 0. +Proof. by rewrite /join /giry_ev /giry_int/= integral0_eq. Qed. + +Let join_ge0 A : 0 <= join A. Proof. by rewrite /join integral_ge0. Qed. + +Let join_semi_sigma_additive : semi_sigma_additive join. +Proof. +move=> F mF tF _; rewrite [X in _ --> X](_ : _ = + giry_int M (fun x => \sum_(0 <= k mu _. + by apply/esym/cvg_lim => //; exact: measure_sigma_additive. +rewrite [X in X @ _](_ : _ = + (fun n => giry_int M (fun mu => \sum_(0 <= i < n) mu (F i)))); last first. + apply/funext => n; rewrite -ge0_integral_sum//. + by move=> ?; exact: measurable_giry_ev. +apply: cvg_monotone_convergence => //. +- by move=> n; apply: emeasurable_sum => m; exact: measurable_giry_ev. +- by move=> n x _; rewrite sume_ge0. +- by move=> x _ m n mn; exact: ereal_nondecreasing_series. +Qed. + +HB.instance Definition _ := isMeasure.Build d _ R join + join0 join_ge0 join_semi_sigma_additive. + +Let join_setT : join [set: T] <= 1. +Proof. +rewrite (@le_trans _ _ (\int[M]_x `|giry_ev x [set: T]|))//; last first. + rewrite (le_trans _ (@sprobability_setT _ _ _ M))//. + rewrite -[leRHS]mul1e integral_le_bound//. + exact: measurable_giry_ev. + by apply/aeW => x _; rewrite gee0_abs// sprobability_setT. +rewrite ge0_le_integral//=. +- exact: measurable_giry_ev. +- by move=> x _; rewrite abse_ge0. +- by apply: measurableT_comp => //; exact: measurable_giry_ev. +- by move=> x _; rewrite gee0_abs. +Qed. + +HB.instance Definition _ := Measure_isSubProbability.Build _ _ _ join join_setT. + +Definition giry_join : giry T R := join. + +End giry_join. +Arguments giry_join {d T R}. + +Section measurable_giry_join. +Context {d} {T : measurableType d} {R : realType}. + +Lemma measurable_giry_join : measurable_fun [set: giry (giry T R) R] giry_join. +Proof. +apply: measurable_giry_codensity => //= B mB. +by apply: measurable_giry_int => //; exact: measurable_giry_ev. +Qed. + +Import HBNNSimple. + +Lemma sintegral_giry_join (M : giry (giry T R) R) (h : {nnsfun T >-> R}) : + sintegral (giry_join M) h = \int[M]_mu sintegral mu h. +Proof. +under eq_integral do rewrite sintegralE. +rewrite ge0_integral_fsum//; last 2 first. + by move=> r; apply: measurable_funeM; exact: measurable_giry_ev. + by move=> n x _; exact: nnsfun_mulemu_ge0. +rewrite sintegralE /=; apply: eq_fsbigr => // r rh. +rewrite integralZl//. +have := finite_measure_integrable_cst M 1 measurableT. +apply: le_integrable => //; first exact: measurable_giry_ev. +move=> mu _ /=. +rewrite normr1 (le_trans _ (@sprobability_setT _ _ _ mu))// gee0_abs//. +by rewrite le_measure// ?inE. +Qed. + +Lemma giry_int_join (M : giry (giry T R) R) (h : T -> \bar R) : + measurable_fun [set: T] h -> (forall x, 0 <= h x) -> + giry_int (giry_join M) h = giry_int M (giry_int ^~ h). +Proof. +move=> mh h0. +pose g := nnsfun_approx measurableT mh. +pose gE := fun n => EFin \o g n. +have mgE n : measurable_fun [set: T] (gE n) by exact/measurable_EFinP. +have gE_ge0 n x : 0 <= gE n x by rewrite lee_fin. +have nd_gE x : {homo gE ^~ x : n m / (n <= m)%O >-> n <= m}. + by move=> *; exact/lefP/nd_nnsfun_approx. +rewrite /giry_int. +transitivity (limn (fun n => \int[giry_join M]_x gE n x)). + rewrite -monotone_convergence//; apply: eq_integral => t _. + by apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. +transitivity (limn (fun n => \int[M]_mu \int[mu]_x gE n x)). + apply: congr_lim; apply/funext => n. + rewrite integralT_nnsfun sintegral_giry_join; apply: eq_integral => x _. + by rewrite integralT_nnsfun. +rewrite -[LHS]monotone_convergence//; last 3 first. + by move=> n; exact: measurable_giry_int. + by move=> n x _; exact: integral_ge0. + by move=> x _ m n mn; apply: ge0_le_integral => // t _; exact: nd_gE. +apply: eq_integral => mu _. +rewrite -monotone_convergence//. +apply: eq_integral => t _. +by apply/cvg_lim => //; exact: cvg_nnsfun_approx. +Qed. + +End measurable_giry_join. + +Section giry_bind. +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). +Implicit Types (mu : giry T1 R) (f : T1 -> giry T2 R). + +Definition giry_bind mu f (mf : measurable_fun [set: T1] f) : giry T2 R := + (giry_join \o giry_map mf) mu. + +Local Notation "m >>= mf" := (giry_bind m mf). + +Lemma measurable_giry_bind f (mf : measurable_fun [set: T1] f) : + measurable_fun [set: giry T1 R] (fun mu => mu >>= mf). +Proof. +apply: (@measurableT_comp _ _ _ _ _ _ _ _ (giry_map mf)) => //=. + exact: measurable_giry_join. +exact: measurable_giry_map. +Qed. + +Lemma giry_int_bind mu f (mf : measurable_fun [set: T1] f) (h : T2 -> \bar R) : + measurable_fun [set: T2] h -> (forall x, 0 <= h x)%E -> + giry_int (mu >>= mf) h = giry_int mu (fun x => giry_int (f x) h). +Proof. +move=> mh h0; rewrite /giry_bind /= giry_int_join// giry_int_map//. + exact: measurable_giry_int. +by move=> ?; exact: integral_ge0. +Qed. + +End giry_bind. + +Section giry_monad. +Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) + (T3 : measurableType d3) (R : realType). + +Lemma giry_joinA (x : giry (giry (giry T1 R) R) R) : + (giry_join \o giry_map measurable_giry_join) x ≡μ + (giry_join \o giry_join) x. +Proof. +move=> A mA/=. +rewrite giry_int_map//; last exact: measurable_giry_ev. +by rewrite giry_int_join//; exact: measurable_giry_ev. +Qed. + +Lemma giry_join_id1 (x : giry T1 R) : + (giry_join \o giry_map measurable_giry_ret) x ≡μ + (giry_join \o giry_ret) x. +Proof. +move=> A mA/=. +rewrite giry_int_map//; last exact: measurable_giry_ev. +rewrite giry_int_ret//; last exact: measurable_giry_ev. +by rewrite /giry_int /giry_ev /giry_ret/= /dirac integral_indic// setIT. +Qed. + +Lemma giry_join_id2 (x : giry (giry T1 R) R) (f : T1 -> T2) + (mf : measurable_fun [set: T1] f) : + (giry_join \o giry_map (measurable_giry_map mf)) x ≡μ + (giry_map mf \o giry_join) x. +Proof. +by move=> X mS /=; rewrite giry_int_map//; exact: measurable_giry_ev. +Qed. + +End giry_monad. + +(* https://en.wikipedia.org/wiki/Giry_monad#Product_distributions *) +Definition giry_prod {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType} (m : giry T1 R * giry T2 R) : giry (T1 * T2)%type R := + @product_subprobability _ _ T1 T2 R m. + +Section measurable_giry_prod. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType}. + +(* See: Tobias Fritz. A synthetic approach to Markov kernels, conditional + independence and theorems on sufficient statistics. + https://arxiv.org/abs/1908.07021 *) +Lemma measurable_giry_prod : + measurable_fun [set: giry T1 R * giry T2 R] giry_prod. +Proof. +apply: measurable_giry_codensity => //=. +rewrite measurable_prod_measurableType. +apply: dynkin_induction => /=. +- by rewrite measurable_prod_measurableType. +- move=> _ _ [A1 mA1 [A2 mA2 <-]] [B1 mB1 [B2 mB2 <-]]. + exists (A1 `&` B1); first exact: measurableI. + exists (A2 `&` B2); first exact: measurableI. + by rewrite setXI. +- apply: (eq_measurable_fun (fun x : giry T1 R * giry T2 R => + x.1 [set: T1] * x.2 [set: T2])). + by move=> x _; rewrite -setXTT product_measure1E. + by apply: emeasurable_funM => /=; + apply: (@measurableT_comp _ _ _ _ _ _ (giry_ev ^~ _)) => //; + exact: measurable_giry_ev. +- move=> _ [A mA [B mB <-]]. + apply: (eq_measurable_fun (fun x : giry T1 R * giry T2 R => x.1 A * x.2 B)). + by move=> x _; rewrite product_measure1E. + by apply: emeasurable_funM; + apply: (@measurableT_comp _ _ _ _ _ _ (giry_ev ^~ _)) => //; + exact: measurable_giry_ev. +- move=> S mS HS. + apply: (eq_measurable_fun (fun x : giry T1 R * giry T2 R => + x.1 [set: T1] * x.2 [set: T2] - (x.1 \x x.2) S)). + move=> /= x _; rewrite product_subprobability_setC//. + by rewrite -setXTT product_measure1E. + apply emeasurable_funB => //=. + by apply: emeasurable_funM => //=; + apply: (@measurableT_comp _ _ _ _ _ _ (giry_ev ^~ _)) => //; + exact: measurable_giry_ev. +- move=> F mF tF Fn. + apply: (eq_measurable_fun (fun x : giry T1 R * giry T2 R => + \sum_(0 <= k x _; rewrite measure_semi_bigcup//; exact: bigcup_measurable. + exact: ge0_emeasurable_sum. +Qed. + +End measurable_giry_prod. + +Section giry_prod_int. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType}. +Variables (m1 : giry T1 R) (m2 : giry T2 R) (h : T1 * T2 -> \bar R). +Hypotheses (mh : measurable_fun [set: T1 * T2] h) (h0 : forall x, 0 <= h x). + +Lemma giry_int_prod1 : giry_int (giry_prod (m1, m2)) h = + giry_int m1 (fun x => giry_int m2 (fun y => h (x, y))). +Proof. exact: fubini_tonelli1. Qed. + +Lemma giry_int_prod2 : giry_int (giry_prod (m1, m2)) h = + giry_int m2 (fun y => giry_int m1 (fun x => h (x, y))). +Proof. exact: fubini_tonelli2. Qed. + +End giry_prod_int. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index 381aa72af2..e4548acab0 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v @@ -25,12 +25,14 @@ From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable. (* *) (* Detailed contents: *) (* ``` *) -(* m1 \x m2 == product measure over T1 * T2, m1 is a measure *) -(* over T1, and m2 is a sigma finite measure over *) -(* T2 *) -(* m1 \x^ m2 == product measure over T1 * T2, m2 is a measure *) -(* over T1, and m1 is a sigma finite measure over *) -(* T2 *) +(* m1 \x m2 == product measure over T1 * T2, m1 is a measure *) +(* over T1, and m2 is a sigma finite measure over *) +(* T2 *) +(* product_subprobability P == P.1 \x P.2 where P is a pair of subprobability *) +(* measures *) +(* m1 \x^ m2 == product measure over T1 * T2, m2 is a measure *) +(* over T1, and m1 is a sigma finite measure over *) +(* T2 *) (* ``` *) (* *) (******************************************************************************) @@ -316,6 +318,48 @@ Qed. End product_measure1E. +Section product_subprobability. +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType}. +Variable m12 : subprobability T1 R * subprobability T2 R. + +Let prod := m12.1 \x m12.2. + +HB.instance Definition _ := Measure.on prod. + +Let prod_setT : prod setT <= 1. +Proof. +rewrite -setXTT [leLHS]product_measure1E// -[leRHS]mule1. +by rewrite lee_pmul// sprobability_setT. +Qed. + +HB.instance Definition _ := + Measure_isSubProbability.Build _ _ _ prod prod_setT. + +Definition product_subprobability : subprobability (T1 * T2)%type R := prod. + +End product_subprobability. + +Section product_subprobability_setC. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. +Context {d1} {d2} {T1 : measurableType d1} {T2 : measurableType d2} + {R : realType}. + +Lemma product_subprobability_setC (P : subprobability T1 R * subprobability T2 R) + (A : set (T1 * T2)) : measurable A -> + (P.1 \x P.2) (~` A) = (P.1 \x P.2) [set: T1 * T2] - (P.1 \x P.2) A. +Proof. +move=> mA. +rewrite -(setvU A) measureU//=; [|exact: measurableC|exact: setICl]. +by rewrite addeK// (_ : (_ \x _)%E = product_subprobability P)// fin_num_measure. +Qed. + +End product_subprobability_setC. + Section product_measure_unique. Local Open Scope ereal_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 72a63b8d61..b52ae7d358 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -1163,6 +1163,32 @@ Proof. by move=> PF; apply: bigcap_measurable => //; exists 1. Qed. End sigmaring_lemmas. +(* Adapted from mathlib induction_on_inter *) +Lemma dynkin_induction d {T : measurableType d} (G : set (set T)) + (P : set_system T) : + @measurable _ T = <> -> + setI_closed G -> + P [set: T] -> + G `<=` P -> + (forall S, measurable S -> P S -> P (~` S)) -> + (forall F : (set T)^nat, + (forall n, measurable (F n)) -> + trivIset [set: nat] F -> + (forall n, P (F n)) -> P (\bigcup_k F k)) -> + (forall S, <> S -> P S). +Proof. +move=> GE GI PsetT GP PsetC Pbigcup A sGA. +suff: <> `<=` [set A | measurable A /\ P A] by move=> /(_ _ sGA)[]. +apply: lambda_system_subset; [by []| | |by []]. +- apply/dynkin_lambda_system; split => //. + + by move=> B [mB PB]; split; [exact: measurableC|exact: PsetC]. + + move=> F tF Hm; split. + by apply: bigcup_measurable => k _; apply Hm. + by apply: Pbigcup => //; apply Hm. +- move=> B GB; split; last exact: GP. + by rewrite GE; exact: sub_gen_smallest. +Qed. + Lemma countable_measurable d (T : sigmaRingType d) (A : set T) : (forall t : T, measurable [set t]) -> countable A -> measurable A. Proof. @@ -1173,7 +1199,6 @@ rewrite [X in _ X](_ : _ = \bigcup_(x in f @` A) [set 'pinv_(cst r) A f x]). by rewrite eqEsubset; split=> [_ [_ [s As <-]] <-|_ [_ [s As <-]] ->]; exists (f s). Qed. - Section sigma_ring_lambda_system. Context d (T : sigmaRingType d). diff --git a/theories/measure_theory/probability_measure.v b/theories/measure_theory/probability_measure.v index 59be2b94a7..adcdb9f54d 100644 --- a/theories/measure_theory/probability_measure.v +++ b/theories/measure_theory/probability_measure.v @@ -73,6 +73,17 @@ HB.instance Definition _ := @isSubProbability.Build _ _ _ P sprobability_setT. HB.end. +Section mzero_subprobability. +Context d (T : measurableType d) (R : realType). + +Let mzero_setT : (@mzero d T R setT <= 1)%E. +Proof. by rewrite /mzero/=. Qed. + +HB.instance Definition _ := + Measure_isSubProbability.Build _ _ _ (@mzero d T R) mzero_setT. + +End mzero_subprobability. + HB.mixin Record isProbability d (T : measurableType d) (R : realType) (P : set T -> \bar R) := { probability_setT : P setT = 1%E }.