diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3bd10f2be8..c52d4873e7 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -7,6 +7,23 @@ - in `topology.v`: + lemma `ball_subspace_ball` +- in `classical_sets.v`: + + lemma `setDU` + +- in `measure.v`: + + definition `completed_measure_extension` + + lemma `completed_measure_extension_sigma_finite` + +- in `lebesgue_stieltjes_measure.v`: + + definition `completed_lebesgue_stieltjes_measure` + +- in `lebesgue_measure.v`: + + definition `completed_lebesgue_measure` + + lemma `completed_lebesgue_measure_is_complete` + + definition `completed_algebra_gen` + + lemmas `g_sigma_completed_algebra_genE`, `negligible_sub_caratheodory`, + `completed_caratheodory_measurable` + ### Changed - in `topology.v`: diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 0360808c37..90d18a5156 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -732,6 +732,16 @@ Qed. Lemma setDKU A B : A `<=` B -> (B `\` A) `|` A = B. Proof. by move=> /setDUK; rewrite setUC. Qed. +Lemma setDU A B C : A `<=` B -> B `<=` C -> C `\` A = (C `\` B) `|` (B `\` A). +Proof. +move=> AB BC; apply/seteqP; split. + move=> x [Cx Ax]. + by have [Bx|Bx] := pselect (B x); [right|left]. +move=> x [[Cx Bx]|[Bx Ax]]. +- by split => // /AB. +- by split => //; exact/BC. +Qed. + Lemma setDv A : A `\` A = set0. Proof. by rewrite predeqE => t; split => // -[]. Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 204e2dcb7f..3a85507b30 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -24,12 +24,15 @@ Require Export lebesgue_stieltjes_measure. (* - Achim Klenke, Probability Theory 2nd edition, 2014 *) (* *) (* ``` *) -(* lebesgue_measure == the Lebesgue measure *) -(* ps_infty == inductive definition of the powerset *) -(* {0, {-oo}, {+oo}, {-oo,+oo}} *) -(* emeasurable G == sigma-algebra over \bar R built out of the *) -(* measurables G of a sigma-algebra over R *) -(* elebesgue_measure == the Lebesgue measure extended to \bar R *) +(* lebesgue_measure == the Lebesgue measure *) +(* completed_lebesgue_measure == the completed Lebesgue measure *) +(* completed_algebra_gen == generator of the completed Lebesgue *) +(* sigma-algebra *) +(* ps_infty == inductive definition of the powerset *) +(* {0, {-oo}, {+oo}, {-oo,+oo}} *) +(* emeasurable G == sigma-algebra over \bar R built out of the *) +(* measurables G of a sigma-algebra over R *) +(* elebesgue_measure == the Lebesgue measure extended to \bar R *) (* ``` *) (* *) (* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs *) @@ -350,11 +353,199 @@ End LebesgueMeasure. Definition lebesgue_measure {R : realType} : set [the measurableType _.-sigma of g_sigma_algebraType R.-ocitv.-measurable] -> \bar R := - [the measure _ _ of lebesgue_stieltjes_measure [the cumulative _ of idfun]]. + [the measure _ _ of lebesgue_stieltjes_measure idfun]. HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). HB.instance Definition _ (R : realType) := SigmaFiniteMeasure.on (@lebesgue_measure R). +Definition completed_lebesgue_measure {R : realType} : set _ -> \bar R := + [the measure _ _ of completed_lebesgue_stieltjes_measure idfun]. +HB.instance Definition _ (R : realType) := + Measure.on (@completed_lebesgue_measure R). +HB.instance Definition _ (R : realType) := + SigmaFiniteMeasure.on (@completed_lebesgue_measure R). + +Lemma completed_lebesgue_measure_is_complete {R : realType} : + measure_is_complete (@completed_lebesgue_measure R). +Proof. exact: measure_is_complete_caratheodory. Qed. + +Definition completed_algebra_gen d {T : semiRingOfSetsType d} {R : realType} + (mu : set T -> \bar R) : set _ := + [set A `|` N | A in d.-measurable & N in mu.-negligible]. + +(* the completed sigma-algebra is the same as the caratheodory sigma-algebra *) +Section completed_algebra_caratheodory. +Context {R : realType}. +Local Open Scope ereal_scope. + +Notation hlength := (@wlength R idfun). +Notation mu := (@lebesgue_measure R). +Notation completed_mu := (@completed_lebesgue_measure R). + +Let cara_sub_calgebra : hlength^*%mu.-cara.-measurable `<=` + (completed_algebra_gen mu).-sigma.-measurable. +Proof. +move=> E; wlog : E / completed_mu E < +oo. + move=> /= wlg. + have /sigma_finiteP[/= F [UFI ndF mF]] := + measure_extension_sigma_finite (@wlength_sigma_finite R idfun). + move=> mE. + rewrite -(setIT E)/= UFI setI_bigcupr; apply: bigcupT_measurable => i. + apply: wlg. + - rewrite (le_lt_trans _ (mF i).2)//= le_measure// inE/=. + + by apply: measurableI => //; apply: sub_caratheodory; exact: (mF i).1. + + by apply: sub_caratheodory; exact: (mF i).1. + - by apply: measurableI => //; apply: sub_caratheodory; exact: (mF i).1. +move=> mEoo /= mE. +have inv0 n : (0 < n.+1%:R^-1 :> R)%R by rewrite invr_gt0. +set S := [set \sum_(0 <= k + exists2 A, @measurable_cover _ (ocitv_type R) E A & + \sum_(0 <= k s0; have : mu E \is a fin_num by rewrite ge0_fin_numE. + by move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [A EA] <-] ?; exists A. +pose A n := projT1 (cid2 (coverE _ (inv0 n))). +have mA k : @measurable_cover _ (ocitv_type R) E (A k). + by rewrite /A; case: cid2. +have mA_E n : + \sum_(0 <= k /subset_trans; apply; apply: subset_bigcup => i _. +have mF_ m : mu (F_ m) < completed_mu E + m.+1%:R^-1%:E. + apply: (le_lt_trans _ (mA_E m)). + apply: (le_trans (outer_measure_sigma_subadditive hlength^*%mu (A m))). + apply: lee_nneseries => // n _. + by rewrite -((measurable_mu_extE hlength) (A m n))//; have [/(_ n)] := mA m. +pose F := \bigcap_n (F_ n). +have FM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) F. + apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. + by apply: sub_sigma_algebra; have [/(_ i)] := mA k. +have EF : E `<=` F by exact: sub_bigcap. +have muEF : completed_mu E = mu F. + apply/eqP; rewrite eq_le le_outer_measure//=. + apply/lee_addgt0Pr => /= _/posnumP[e]; near \oo => n. + apply: (@le_trans _ _ (mu (F_ n))). + by apply: le_outer_measure; exact: bigcap_inf. + rewrite (le_trans (ltW (mF_ n)))// leeD// lee_fin ltW//. + by near: n; apply: near_infty_natSinv_lt. +have coverEF s : (0 < s)%R -> + exists2 A, @measurable_cover _ (ocitv_type R) (F `\` E) A & + \sum_(0 <= k s0. + have : mu (F `\` E) \is a fin_num. + rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu F))//; last by rewrite -muEF. + by apply: le_outer_measure; exact: subDsetl. + by move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [B FEB] <-] ?; exists B. +pose B n := projT1 (cid2 (coverEF _ (inv0 n))). +have mB k : @measurable_cover _ (ocitv_type R) (F `\` E) (B k). + by rewrite /B; case: cid2. +have mB_FE n : + \sum_(0 <= k /subset_trans; apply; apply: subset_bigcup => i _. +have mG_ m : mu (G_ m) < completed_mu (F `\` E) + m.+1%:R^-1%:E. + apply: (le_lt_trans _ (mB_FE m)). + apply: (le_trans (outer_measure_sigma_subadditive hlength^*%mu (B m))). + apply: lee_nneseries => // n _. + by rewrite -((measurable_mu_extE hlength) (B m n))//; have [/(_ n)] := mB m. +pose G := \bigcap_n (G_ n). +have GM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) G. + apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. + by apply: sub_sigma_algebra; have [/(_ i)] := mB k. +have FEG : F `\` E `<=` G by exact: sub_bigcap. +have muG : mu G = 0. + transitivity (completed_mu (F `\` E)). + apply/eqP; rewrite eq_le; apply/andP; split; last exact: le_outer_measure. + apply/lee_addgt0Pr => _/posnumP[e]. + near \oo => n. + apply: (@le_trans _ _ (mu (G_ n))). + by apply: le_outer_measure; exact: bigcap_inf. + rewrite (le_trans (ltW (mG_ n)))// leeD// lee_fin ltW//. + by near: n; apply: near_infty_natSinv_lt. + rewrite measureD//=. + + by rewrite setIidr// muEF subee// ge0_fin_numE//; move: mEoo; rewrite muEF. + + exact: sub_caratheodory. + + by move: mEoo; rewrite muEF. +apply: sub_sigma_algebra; exists (F `\` G); first exact: measurableD. +exists (E `&` G). + by apply: (@negligibleS _ _ _ mu G _ (@subIsetr _ E G)); exists G; split. +apply/seteqP; split=> [/= x [[Fx Gx]|[]//]|x Ex]. +- by rewrite -(notK (E x)) => Ex; apply: Gx; exact: FEG. +- have [|FGx] := pselect ((F `\` G) x); first by left. + right; split => //. + move/not_andP : FGx => [|]. + by have := EF _ Ex. + by rewrite notK. +Unshelve. all: by end_near. Qed. + +Lemma g_sigma_completed_algebra_genE : + (completed_algebra_gen mu).-sigma.-measurable = completed_algebra_gen mu. +Proof. +apply/seteqP; split; last first. + move=> _ [/= A /= mA [N neglN]] <-. + by apply: sub_sigma_algebra; exists A => //; exists N. +apply: smallest_sub => //=; split => /=. +- by exists set0 => //; exists set0; [exact: negligible_set0|rewrite setU0]. +- move=> G [/= A mA [N negN ANG]]; case: negN => /= F [mF F0 NF]. + have GANA : ~` G = ~` A `\` (N `&` ~` A). + by rewrite -ANG setCU setDE setCI setCK setIUr setICl setU0. + pose AA := ~` A `\` (F `&` ~` A). + pose NN := (F `&` ~` A) `\` (N `&` ~` A). + have GAANN : ~` G = AA `|` NN. + rewrite (_ : ~` G = ~` A `\` (N `&` ~` A))//. + by apply: setDU; [exact: setSI|exact: subIsetr]. + exists AA. + apply: measurableI => //=; first exact: measurableC. + by apply: measurableC; apply: measurableI => //; exact: measurableC. + by exists NN; [exists F; split => // x [] []|rewrite setDE setTI]. +- move=> F mF/=. + pose A n := projT1 (cid2 (mF n)). + pose N n := projT1 (cid2 (projT2 (cid2 (mF n))).2). + exists (\bigcup_k A k). + by apply: bigcupT_measurable => i; rewrite /A; case: cid2. + exists (\bigcup_k N k). + apply: negligible_bigcup => /= k. + by rewrite /N; case: (cid2 (mF k)) => //= *; case: cid2. + rewrite -bigcupU; apply: eq_bigcup => // i _. + by rewrite /A /N; case: (cid2 (mF i)) => //= *; case: cid2. +Qed. + +Lemma negligible_sub_caratheodory : + completed_mu.-negligible `<=` hlength^*%mu.-cara.-measurable. +Proof. +move=> N /= [/= A] [mA A0 NA]. +apply: le_caratheodory_measurable => /= X. +apply: (@le_trans _ _ (hlength^*%mu N + hlength^*%mu (X `&` ~` N))). + by rewrite leeD2r// le_outer_measure//; exact: subIsetr. +have -> : hlength^*%mu N = 0. + by apply/eqP; rewrite eq_le outer_measure_ge0//= andbT -A0 le_outer_measure. +by rewrite add0e// le_outer_measure//; exact: subIsetl. +Qed. + +Let calgebra_sub_cara : (completed_algebra_gen mu).-sigma.-measurable `<=` + hlength^*%mu.-cara.-measurable. +Proof. +rewrite g_sigma_completed_algebra_genE => A -[/= X mX] [N negN] <-{A}. +apply: measurableU => //; first exact: sub_caratheodory. +apply: negligible_sub_caratheodory; case: negN => /= B [mB B0 NB]. +by exists B; split => //=; exact: sub_caratheodory. +Qed. + +Lemma completed_caratheodory_measurable : + (completed_algebra_gen mu).-sigma.-measurable = + hlength^*%mu.-cara.-measurable. +Proof. +by apply/seteqP; split; [exact: calgebra_sub_cara | exact: cara_sub_calgebra]. +Qed. + +End completed_algebra_caratheodory. + Section ps_infty. Context {T : Type}. Local Open Scope ereal_scope. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 4a29cb6577..f4c6d42170 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -17,20 +17,22 @@ Require Import real_interval measure realfun. (* - Achim Klenke, Probability Theory 2nd edition, 2014 *) (* *) (* ``` *) -(* right_continuous f == the function f is right-continuous *) -(* cumulative R == type of non-decreasing, right-continuous *) -(* functions (with R : numFieldType) *) -(* The HB class is Cumulative. *) -(* instance: idfun *) -(* ocitv_type R == alias for R : realType *) -(* ocitv == set of open-closed intervals ]x, y] where *) -(* x and y are real numbers *) -(* R.-ocitv == display for ocitv_type R *) -(* R.-ocitv.-measurable == semiring of sets of open-closed intervals *) -(* wlength f A := f b - f a with the hull of the set of real *) -(* numbers A being delimited by a and b *) +(* right_continuous f == the function f is right-continuous *) +(* cumulative R == type of non-decreasing, right-continuous *) +(* functions (with R : numFieldType) *) +(* The HB class is Cumulative. *) +(* instance: idfun *) +(* ocitv_type R == alias for R : realType *) +(* ocitv == set of open-closed intervals ]x, y] where *) +(* x and y are real numbers *) +(* R.-ocitv == display for ocitv_type R *) +(* R.-ocitv.-measurable == semiring of sets of open-closed intervals *) +(* wlength f A := f b - f a with the hull of the set of real *) +(* numbers A being delimited by a and b *) (* lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f *) -(* f is a cumulative function. *) +(* f is a cumulative function. *) +(* completed_lebesgue_stieltjes_measure f == the completed Lebesgue-Stieltjes *) +(* measure *) (* ``` *) (* *) (******************************************************************************) @@ -523,3 +525,24 @@ by move=> A mA; rewrite -muE// -measurable_mu_extE. Qed. End lebesgue_stieltjes_measure. + +Section completed_lebesgue_stieltjes_measure. +Context {R : realType}. + +Definition completed_lebesgue_stieltjes_measure (f : cumulative R) := + @completed_measure_extension _ _ _ [the measure _ _ of wlength f]. + +HB.instance Definition _ (f : cumulative R) := + Measure.on (@completed_lebesgue_stieltjes_measure f). + +Let sigmaT_finite_completed_lebesgue_stieltjes_measure (f : cumulative R) : + sigma_finite setT (@completed_lebesgue_stieltjes_measure f). +Proof. exact/completed_measure_extension_sigma_finite/wlength_sigma_finite. Qed. + +HB.instance Definition _ (f : cumulative R) := + @Measure_isSigmaFinite.Build _ _ _ + (@completed_lebesgue_stieltjes_measure f) + (sigmaT_finite_completed_lebesgue_stieltjes_measure f). + +End completed_lebesgue_stieltjes_measure. +Arguments completed_lebesgue_stieltjes_measure {R}. diff --git a/theories/measure.v b/theories/measure.v index 25ff40621a..59f84235dc 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -250,6 +250,8 @@ From HB Require Import structures. (* sets to a measure over the generated *) (* sigma algebra (requires a proof of *) (* sigma-sub-additivity) *) +(* completed_measure_extension mu == similar to measure_extension but returns *) +(* a complete measure *) (* ``` *) (* *) (* ## Product of measurable spaces *) @@ -4813,6 +4815,45 @@ Proof. by move=> Am; apply: sub_caratheodory => //; apply: sub_sigma_algebra. Qed. +Section completed_measure_extension. +Local Open Scope ereal_scope. +Context d (T : semiRingOfSetsType d) (R : realType). +Variable mu : {measure set T -> \bar R}. +Notation rT := (SetRing.type T). +Let Rmu : set rT -> \bar R := SetRing.measure mu. + +Let I := [the measurableType _ of caratheodory_type (mu^*)%mu]. + +Definition completed_measure_extension : set I -> \bar R := (mu^*)%mu. + +Let measure0 : completed_measure_extension set0 = 0. +Proof. exact: mu_ext0. Qed. + +Let measure_ge0 (A : set I) : 0 <= completed_measure_extension A. +Proof. exact: mu_ext_ge0. Qed. + +Let measure_semi_sigma_additive : + semi_sigma_additive completed_measure_extension. +Proof. +move=> F mF tF mUF; rewrite /completed_measure_extension. +exact: caratheodory_measure_sigma_additive. +Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ completed_measure_extension + measure0 measure_ge0 measure_semi_sigma_additive. + +Lemma completed_measure_extension_sigma_finite : @sigma_finite _ T _ setT mu -> + @sigma_finite _ _ _ setT completed_measure_extension. +Proof. +move=> -[S setTS mS]; exists S => //; move=> i; split. +- apply: sub_caratheodory; apply: sub_sigma_algebra. + exact: (mS i).1. +- by rewrite /completed_measure_extension /= measurable_mu_extE //; + [exact: (mS i).2 | exact: (mS i).1]. +Qed. + +End completed_measure_extension. + Definition preimage_classes d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2) (T : Type) (f1 : T -> T1) (f2 : T -> T2) :=