rm cmu

theories/absolute_continuity.v

@@ -641,332 +641,6 @@ split.
 - by move=> Hmu A [B [mB B0 AB]]; exact: Hmu AB.
 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.
-
-
-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}.
-
-
-Definition completed_lebesgue_measure {R : realType} : set _ -> \bar R :=
-  [the measure _ _ of
-    completed_lebesgue_stieltjes_measure [the cumulative _ of 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_measureE {R : realType} :
-  (@completed_lebesgue_measure R) = (@lebesgue_measure R).
-Proof. by []. Qed.
-
-Lemma sigma_algebra_mu_ext {R : realType} :
-  sigma_algebra [set: ocitv_type R] (wlength idfun)^*%mu.-cara.-measurable.
-Proof.
-split.
-- exact: caratheodory_measurable_set0.
-- by move=> A mA; rewrite setTD; exact: caratheodory_measurable_setC.
-- by move=> F mF; exact: caratheodory_measurable_bigcup.
-Qed.
-
-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].
-
-(*Definition completed_algebra d {T : semiRingOfSetsType d} {R : realType}
-    (mu : set T -> \bar R) : measurableType _ :=
-  salgebraType (completed_algebra_gen mu).*)
-
-Lemma setDU {T} (U V W : set T) : U `<=` V -> V `<=` W ->
-  W `\` U = (W `\` V) `|` (V `\` U).
-Proof.
-move=> UV VW; apply/seteqP; split.
-  move=> x [Wx Ux].
-  by have [Vx|Vx] := pselect (V x); [right|left].
-move=> x [[Wx Vx]|[Vx Ux]].
-- by split => // /UV.
-- by split => //; exact/VW.
-Qed.
-
-(* the completed sigma-algebra is the same as the caratheodory sigma-algebra *)
-Section completed_algebra_cara.
-Context {R : realType}.
-
-Let cara_sub_calgebra : ((wlength idfun)^*)%mu.-cara.-measurable `<=`
-  (completed_algebra_gen (@lebesgue_measure R)).-sigma.-measurable.
-Proof.
-move=> E.
-wlog : E / (completed_lebesgue_measure E < +oo)%E.
-  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 by rewrite invr_gt0.
-set S :=
-  [set (\sum_(0 <= k <oo) wlength idfun (A k))%E | A in measurable_cover E].
-have H1 s : 0 < s ->
-     exists2 A_ : (set R) ^nat,
-       @measurable_cover _ (ocitv_type R) E A_ &
-       (\sum_(0 <= k <oo) wlength idfun (A_ k) <
-        completed_lebesgue_measure E + s%:E)%E.
-  move=> s0.
-  have : lebesgue_measure E \is a fin_num by rewrite ge0_fin_numE.
-  move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [A_ EA_] <-] ?.
-  by exists A_.
-pose A_ n := projT1 (cid2 (H1 _ (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) wlength idfun (A_ n k) <
-    completed_lebesgue_measure E + n.+1%:R^-1%:E)%E.
-  by rewrite /A_; case: cid2.
-pose F_ n := \bigcup_m (A_ n m).
-have EF_n n : E `<=` F_ n.
-  have [/= _] := mA n.
-  move=> /subset_trans; apply.
-  by apply: subset_bigcup => i _.
-have mF_ m : (lebesgue_measure (F_ m) <
-    completed_lebesgue_measure E + m.+1%:R^-1%:E)%E.
-  apply: (le_lt_trans _ (mA_E m)).
-  rewrite /lebesgue_measure/= /lebesgue_stieltjes_measure/= /measure_extension/=.
-  apply: (le_trans
-   (outer_measure_sigma_subadditive (@wlength R idfun)^*%mu (A_ m))).
-  apply: lee_nneseries => // n _.
-  rewrite -((measurable_mu_extE (@wlength R idfun)) (A_ m n))//.
-  by have [/(_ n)] := mA m.
-pose F := \bigcap_n (F_ n).
-have FM : @measurable _ (salgebraType 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_lebesgue_measure E = lebesgue_measure F.
-  apply/eqP; rewrite eq_le; apply/andP; split.
-    by rewrite le_outer_measure.
-  apply/lee_addgt0Pr => /= _/posnumP[e].
-  near \oo => n.
-  apply: (@le_trans _ _ (lebesgue_measure (F_ n))).
-    by apply: le_outer_measure; exact: bigcap_inf.
-  apply: (le_trans (ltW (mF_ n))).
-  rewrite leeD// lee_fin ltW//.
-  by near: n; apply: near_infty_natSinv_lt.
-have H2 (s : R) : 0 < s ->
-     exists2 A_ : (set R) ^nat,
-       @measurable_cover _ (ocitv_type R) (F `\` E) A_ &
-       (\sum_(0 <= k <oo) wlength idfun (A_ k) <
-        completed_lebesgue_measure (F `\` E) + s%:E)%E.
-  move=> s0.
-  have : lebesgue_measure (F `\` E) \is a fin_num.
-    rewrite ge0_fin_numE// (@le_lt_trans _ _ (lebesgue_measure F))//.
-      by apply: le_outer_measure; exact: subDsetl.
-    by rewrite -muEF.
-  move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [B_ FEB_] <-] ?.
-  by exists B_.
-pose B_ n := projT1 (cid2 (H2 _ (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) wlength idfun (B_ n k) <
-        completed_lebesgue_measure (F `\` E) + n.+1%:R^-1%:E)%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.
-  move=> /subset_trans; apply.
-  by apply: subset_bigcup => i _.
-have mG_ m : (lebesgue_measure (G_ m) <
-             completed_lebesgue_measure (F `\` E) + m.+1%:R^-1%:E)%E.
-  apply: (le_lt_trans _ (mB_FE m)).
-  rewrite /lebesgue_measure/= /lebesgue_stieltjes_measure/= /measure_extension/=.
-  apply: (le_trans (outer_measure_sigma_subadditive (@wlength R idfun)^*%mu (B_ m))).
-  apply: lee_nneseries => // n _.
-  have <-// := (measurable_mu_extE (@wlength R idfun)) (B_ m n).
-  by have [/(_ n)] := mB m.
-pose G := \bigcap_n (G_ n).
-have GM : @measurable _ (salgebraType 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 : lebesgue_measure G = 0.
-  transitivity (completed_lebesgue_measure (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 _ _ (lebesgue_measure (G_ n))).
-      by apply: le_outer_measure; exact: bigcap_inf.
-    apply/ltW/(lt_le_trans (mG_ n)).
-    rewrite leeD// lee_fin ltW//.
-    by near: n; apply: near_infty_natSinv_lt.
-  rewrite measureD//=.
-  + rewrite setIidr// muEF subee// ge0_fin_numE//.
-    by 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).
-  apply: (@negligibleS _ _ _ lebesgue_measure G).
-    exact: subIsetr.
-  by exists G; split.
-apply/seteqP; split=> [/= x [[Fx Gx]|[]//]|x Ex].
-- rewrite -(notK (E x)) => Ex.
-  by 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 completed_salgebra_lebesgue_measure :
-  (completed_algebra_gen (@lebesgue_measure R)).-sigma.-measurable =
-  @completed_algebra_gen _ _ R (@lebesgue_measure R).
-Proof.
-apply/seteqP; split; last first.
-  move=> X [/= A /= mA [N neglN]] <-{X}.
-  apply: sub_sigma_algebra.
-  by exists A => //; exists N.
-apply: smallest_sub => //=; split => /=.
-- exists set0 => //; exists set0 => //; first exact: negligible_set0.
-  by rewrite setU0.
-- move=> G [/= A mA [N negN ANG]].
-  case: negN => /= F [mF F0 NF].
-  have H1 : ~` 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 H2 : ~` 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.
-  exists NN.
-    by exists F; split => // x [] [].
-  by rewrite setDE setTI.
-- move=> F mF/=.
-  rewrite /completed_algebra_gen/=.
-  pose A n := projT1 (cid2 (mF n)).
-  pose N n := projT1 (cid2 (projT2 (cid2 (mF n))).2).
-  exists (\bigcup_k A k).
-    apply: bigcupT_measurable => i.
-    by rewrite /A; case: cid2 => //.
-  exists (\bigcup_k N k).
-    apply: negligible_bigcup => /= k.
-    rewrite /N; case: (cid2 (mF k)) => //= *.
-    by case: cid2 => //.
-  rewrite -bigcupU.
-  apply: eq_bigcup => // i _.
-  rewrite /A /N; case: (cid2 (mF i)) => //= *.
-  by case: cid2 => //=.
-Qed.
-
-Lemma negligible_sub_caratheodory :
-  (@completed_lebesgue_measure R).-negligible `<=`
-  ((wlength idfun)^*)%mu.-cara.-measurable.
-Proof.
-move=> N /= [/= A] [mA A0 NA].
-have H1 : ((wlength idfun)^*)%mu N = 0.
-  apply/eqP; rewrite eq_le; apply/andP; split.
-    rewrite -A0.
-    rewrite (_ : completed_lebesgue_measure A = ((wlength idfun)^*)%mu A)//.
-    by apply: le_outer_measure.
-  exact: outer_measure_ge0.
-apply: le_caratheodory_measurable => /= X.
-apply: (@le_trans _ _ (((wlength idfun)^*)%mu (N) +
-   ((wlength idfun)^*)%mu (X `&` ~` N))).
-  rewrite leeD2r//.
-  apply: le_outer_measure.
-  exact: subIsetr.
-rewrite H1 add0e.
-apply: le_outer_measure.
-exact: subIsetl.
-Qed.
-
-Let calgebra_sub_cara :
-  (completed_algebra_gen (@lebesgue_measure R)).-sigma.-measurable `<=`
-  ((wlength idfun)^*)%mu.-cara.-measurable.
-Proof.
-rewrite completed_salgebra_lebesgue_measure => 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 (@lebesgue_measure R)).-sigma.-measurable =
-  (wlength idfun)^*%mu.-cara.-measurable.
-Proof.
-by apply/seteqP; split => /=;
-  [exact: calgebra_sub_cara|exact: cara_sub_calgebra].
-Qed.
-
-End completed_algebra_cara.
-
 (*mu^*(A)=0 -> A satisfies caratheodory criterion
 
 https://math.stackexchange.com/questions/2913728/complete-measures-and-complete-sigma-algebras*)
@@ -1481,6 +1155,10 @@ End wip.
 Lemma lebesgue_measureT {R : realType} : (@lebesgue_measure R) setT = +oo%E.
 Proof. by rewrite -set_itv_infty_infty lebesgue_measure_itv. Qed.
 
+Lemma completed_lebesgue_measureE {R : realType} :
+  (@completed_lebesgue_measure R) = (@lebesgue_measure R).
+Proof. by []. Qed.
+
 Lemma completed_lebesgue_measure_itv {R : realType} (i : interval R) :
   completed_lebesgue_measure ([set` i] : set R) =
   (if i.1 < i.2 then (i.2 : \bar R) - i.1 else 0)%E.