identifier for completed lebesgue measure

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`:

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.
 

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 <oo) hlength (A k) | A in measurable_cover E].
+have coverE s : (0 < s)%R ->
+   exists2 A, @measurable_cover _ (ocitv_type R) E A &
+   \sum_(0 <= k <oo) hlength (A k) < completed_mu E + s%:E.
+  move=> 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 <oo) hlength (A n k) < completed_mu E + n.+1%:R^-1%:E.
+  by rewrite /A; case: cid2.
+pose F_ n := \bigcup_m (A n m).
+have EF_n n : E `<=` F_ n.
+  have [/= _] := mA n.
+  by move=> /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 <oo) hlength (A k) < completed_mu (F `\` E) + s%:E.
+  move=> 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 <oo) hlength (B n k) < completed_mu (F `\` E) + n.+1%:R^-1%:E.
+  by rewrite /B; case: cid2.
+pose G_ n := \bigcup_m (B n m).
+have FEG_n n : F `\` E `<=` G_ n.
+  have [/= _] := mB n.
+  by move=> /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.

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}.

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)  :=