diff --git a/theories/absolute_continuity.v b/theories/absolute_continuity.v index c13f3a347..8921bd330 100644 --- a/theories/absolute_continuity.v +++ b/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 - exists2 A_ : (set R) ^nat, - @measurable_cover _ (ocitv_type R) E A_ & - (\sum_(0 <= k 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 /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 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 /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.