From 0cbfc1fc0be1cda65e0eb75a4d79d19b3a314ad0 Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 27 Aug 2023 11:52:26 -0400 Subject: [PATCH 1/8] simple functions are bounded --- theories/lebesgue_integral.v | 47 +++++++++++++++++++++++++++++++++++- 1 file changed, 46 insertions(+), 1 deletion(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 2013f246f..1d3d07d62 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -400,6 +400,27 @@ rewrite /preimage /= => [fxfy gzf]. by rewrite gzf -fxfy addrC subrK. Qed. +Section simple_bounded. +Context d (T : measurableType d) (R : realType). + +Lemma simple_bounded {f : {sfun T >-> R}} : + bounded_fun (f : T -> [normedModType R of R^o]). +Proof. +case/finite_seqP:(@fimfunP _ _ f) => r fr. +exists (fine (\big[maxe/-oo%E]_(i <- r) (`|i|)%:E)). +split; rewrite ?num_real // => x mx z _; apply: ltW; apply: (le_lt_trans _ mx). +rewrite (_ : normr (f z) = fine (EFin (normr (f z)))) // fine_le //; first last. +have fzr : (f z \in r) by (have : (range f) (f z) by exists z); rewrite fr. + by rewrite (big_rem _ fzr) /= le_maxr; apply/orP; left. +have fpr : (exists p, p \in r). + by exists (f point); (have : (range f) (f point) by exists point); rewrite fr. +elim: r fpr {fr mx}; first by case => ?. +move=> a l IH _; case: (pselect (exists p, p \in l)). + by move/IH => bfin; rewrite big_cons /maxe; case: (_ < _)%E; rewrite ?bfin. +move=> npl; suff : l == [::] by move/eqP ->; rewrite big_seq1. +rewrite -set_seq_eq0; apply/eqP; rewrite -subset0; move/forallNP: npl; apply. +Qed. + Section nnsfun_functions. Context d (T : measurableType d) (R : realType). @@ -4819,9 +4840,33 @@ rewrite !ger0_norm ?fine_ge0 ?integral_ge0 ?fine_le//. + by apply: emeasurable_funD; [move: mfp | move: mfn]; case/integrableP. + by move=> ? ?; rewrite fpn; exact: lee_abs_sub. Unshelve. all: by end_near. Qed. - End simple_density_L1. +Section continuous_density_L1. +Local Open Scope ereal_scope. +Context (rT : realType). +Let mu := [the measure _ _ of @lebesgue_measure rT]. +Let R := [the measurableType _ of measurableTypeR rT]. +Lemma approximation_continuous_sfun (E : set R) (f : {sfun R >-> rT}): + measurable E -> mu E < +oo -> exists g_ : (rT -> rT)^nat, + [/\ forall n, continuous (g_ n : R -> R), + forall n, mu.-integrable E (EFin \o g_ n) & + (fun n => \int[mu]_(z in E) `|(f z - g_ n z)%:E|) --> 0]. +Proof. +move=> mE Efin. +have : (exists M, 0 < M /\ forall x, `|f x| <= M)%R. + + + Search FImFun.type. +have : forall n, exists (g : rT -> rT), + continuous g /\ \int[mu]_(z in E) `|(f z - g z)%:E| < ((1/n)%R%:E). + move=> n. +Search (exists (_ : (_ -> _)), _) "choice". + + + + + Section fubini_functions. Local Open Scope ereal_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). From c3af94d3c1dcf3c8a8da1d24e3bca5edb16eca25 Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 27 Aug 2023 14:58:16 -0400 Subject: [PATCH 2/8] continuous functions dense in simple --- theories/lebesgue_integral.v | 137 ++++++++++++++++++++++++++--------- 1 file changed, 104 insertions(+), 33 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 1d3d07d62..4f5fd5087 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -420,6 +420,7 @@ move=> a l IH _; case: (pselect (exists p, p \in l)). move=> npl; suff : l == [::] by move/eqP ->; rewrite big_seq1. rewrite -set_seq_eq0; apply/eqP; rewrite -subset0; move/forallNP: npl; apply. Qed. +End simple_bounded. Section nnsfun_functions. Context d (T : measurableType d) (R : realType). @@ -4762,6 +4763,19 @@ Section simple_density_L1. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (E : set T) (mE : measurable E). +Lemma measurable_bounded_integrable (f : T -> R^o) : + (mu E < +oo)%E -> measurable_fun E f -> + [bounded f x | x in E] -> mu.-integrable E (EFin \o f). +Proof. +move=> Afin mfA bdA; apply/integrableP; split. + exact/EFin_measurable_fun. +have [M [_ mrt]] := bdA; apply: le_lt_trans. + apply (@integral_le_bound _ _ _ _ _ _ (`|M| + 1)%:E) => //. + by apply: measurableT_comp => //; exact: subspace_continuous_measurable_fun. + by apply: aeW => z Az; rewrite lee_fin mrt // ltr_pwDr // ler_norm. +by rewrite lte_mul_pinfty. +Qed. + Local Open Scope ereal_scope. Let sfun_dense_L1_pos (f : T -> \bar R) : @@ -4843,29 +4857,104 @@ Unshelve. all: by end_near. Qed. End simple_density_L1. Section continuous_density_L1. -Local Open Scope ereal_scope. Context (rT : realType). Let mu := [the measure _ _ of @lebesgue_measure rT]. Let R := [the measurableType _ of measurableTypeR rT]. -Lemma approximation_continuous_sfun (E : set R) (f : {sfun R >-> rT}): + +Lemma compact_finite_measure (A : set R^o) : + compact A -> (mu A < +oo)%E. +Proof. +move => /[dup]/compact_measurable => ?; case/compact_bounded => N [_ N1x]. +have AN1 : A `<=` `[- (`|N| + 1), `|N| + 1]. + by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_spaddr// ler_norm. +apply: le_lt_trans; first apply: (le_measure _ _ _ AN1); first exact /mem_set. + by apply/mem_set; exact: measurable_itv. +rewrite /= lebesgue_measure_itv hlength_itv /= -fun_if. +by case E : (_%:E < _%:E)%E => //=; rewrite ltry. +Qed. + +Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) : + compact A -> {within A, continuous f} -> mu.-integrable A (EFin \o f). +Proof. +move=> cptA ctsfA; apply: measurable_bounded_integrable. +- exact: compact_measurable. +- exact: compact_finite_measure. +- by apply: subspace_continuous_measurable_fun => //; exact: compact_measurable. +- have /compact_bounded [M [_ mrt]] := continuous_compact ctsfA cptA. + by exists M; split; rewrite ?num_real // => ? ? ? ?; exact: mrt. +Qed. + +Lemma cvge_harmonic : (EFin \o (@harmonic rT)) @ \oo --> 0%E. +Proof. by apply: cvg_EFin; [exact: nearW | exact: cvg_harmonic]. Qed. + +Local Open Scope ereal_scope. +Local Lemma approximation_continuous_sfun (E : set R) (f : {sfun R >-> rT}): measurable E -> mu E < +oo -> exists g_ : (rT -> rT)^nat, [/\ forall n, continuous (g_ n : R -> R), forall n, mu.-integrable E (EFin \o g_ n) & (fun n => \int[mu]_(z in E) `|(f z - g_ n z)%:E|) --> 0]. Proof. -move=> mE Efin. -have : (exists M, 0 < M /\ forall x, `|f x| <= M)%R. - - - Search FImFun.type. -have : forall n, exists (g : rT -> rT), - continuous g /\ \int[mu]_(z in E) `|(f z - g z)%:E| < ((1/n)%R%:E). - move=> n. -Search (exists (_ : (_ -> _)), _) "choice". - - - - +move=> mE Efin; have : (exists M, 0 < M /\ forall x, `|f x| <= M)%R. + case: (@simple_bounded _ _ _ f) => M [_ /= bdM]. + exists (`|M| + 1)%R; split; first exact: ltr_wpDl. + by move=> x; apply: bdM => //; apply: ltr_pwDr; rewrite // ler_norm. +have mf : measurable_fun E f. + apply: (measurable_funS measurableT) => // ? /= ?; rewrite setTI. +case=> M [Mpos Mbd]. +have apxf eps : exists (g : rT -> rT), (eps > 0)%R -> + [/\ continuous g, + mu.-integrable E (EFin \o g) & + \int[mu]_(z in E) `|(f z - g z)%:E| < eps%:E]. + case epspos: (0 < eps)%R; last by exists point. + move: eps epspos => _/posnumP[eps]. + have [] // := @measurable_almost_continuous rT E mE _ f (eps%:num/(M *+ 2)). + by apply: divr_gt0 => //; apply: mulrn_wgt0. + move=> A [cptA AE /= muAE ctsAF]. + have [] := continuous_bounded_extension _ _ Mpos ctsAF. + - exact: pseudometric_normal. + - by apply: compact_closed => //; exact: Rhausdorff . + - by move=> ? ?; exact: Mbd. + have mA : measurable A by exact: compact_measurable. + move=> g [fg ctsg gbdM]; have mg : measurable_fun E g. + apply: subspace_continuous_measurable_fun => //. + exact: continuous_subspaceT. + have intg : mu.-integrable E (EFin \o g). + apply: measurable_bounded_integrable => //. + exists M; split; rewrite ?num_real // => ? sx ? ? /=. + by apply: ltW; apply: (le_lt_trans _ sx); apply: gbdM. + exists g; split => //; rewrite -(setDKU AE) integral_setU => //; first last. + - by rewrite /disj_set setDKI. + - rewrite setDKU //; (do 2 (apply: measurableT_comp => //)). + exact: measurable_funB. + - exact: measurableD. + rewrite (@ae_eq_integral _ _ _ mu A (fun=> 0)) //; first last. + - by apply: aeW => z Az; rewrite (fg z) ?inE // subrr normr0. + - apply: (measurable_funS mE) => //; (do 2 (apply: measurableT_comp => //)). + exact: measurable_funB. + rewrite integral0 adde0; under eq_fun => ? do rewrite -[EFin _]gee0_abs //. + apply: le_lt_trans; first apply: (@integral_le_bound _ _ _ _ _ _ (M *+ 2)%:E). + - exact: measurableD. + - apply: (measurable_funS mE) => //; (do 2 (apply: measurableT_comp => //)). + exact: measurable_funB. + - by rewrite lee_fin mulrn_wge0 //; apply: ltW. + - apply: aeW => z [Ez _]; rewrite /= normr_id lee_fin mulr2n. + apply: le_trans; first exact: ler_normB. + by apply: lerD; [exact: Mbd | exact: gbdM]. + by rewrite -lte_pdivl_mull ? mulrn_wgt0 // muleC -EFinM. +pose g_ (n : nat) := projT1 (cid (apxf (n.+1%:R^-1))); exists g_; split. +- by move=> n; have [] := projT2 (cid (apxf (n.+1%:R^-1))) => //. +- by move=> n; have [] := projT2 (cid (apxf (n.+1%:R^-1))) => //. +apply/cvg_ballP => eps epspos. +have /cvg_ballP/(_ eps epspos) [N _ Nball] := cvge_harmonic. +exists N => //; apply: (subset_trans Nball) => n. +rewrite /ball /= /ereal_ball contract0 ?mul0r ?sub0r ?normrN. +move/(lt_trans _); apply; rewrite ?ger0_norm; first last. +- by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0 integral_ge0. +- by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0. +have [] := projT2 (cid (apxf (n.+1%:R^-1))) => // ? ? ?. +by rewrite -lt_expandRL // ?contractK // inE contract_le1. +Qed. +Section continuous_density_L1. Section fubini_functions. Local Open Scope ereal_scope. @@ -5438,24 +5527,6 @@ Context (rT : realType). Let mu := [the measure _ _ of @lebesgue_measure rT]. Let R := [the measurableType _ of measurableTypeR rT]. -Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) : - compact A -> {within A, continuous f} -> mu.-integrable A (EFin \o f). -Proof. -move=> cptA ctsfA; have mA := compact_measurable cptA; apply/integrableP; split. - by apply: measurableT_comp => //; exact: subspace_continuous_measurable_fun. -have /compact_bounded [M [_ mrt]] := continuous_compact ctsfA cptA. -apply: le_lt_trans. - apply (@integral_le_bound _ _ _ _ _ _ (`|M| + 1)%:E) => //. - by apply: measurableT_comp => //; exact: subspace_continuous_measurable_fun. - by apply: aeW => /= z Az; rewrite lee_fin mrt // ltr_spaddr// ler_norm. -case/compact_bounded : cptA => N [_ N1x]. -have AN1 : A `<=` `[- (`|N| + 1), `|N| + 1]. - by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_spaddr// ler_norm. -apply: (@le_lt_trans _ _ (_ * _)%E). - by rewrite lee_pmul; last by apply: (le_measure _ _ _ AN1); rewrite inE. -by rewrite /= lebesgue_measure_itv hlength_itv /= -fun_if -EFinM ltry. -Qed. - Let ballE (x : R) (r : {posnum rT}) : ball x r%:num = `](x - r%:num), (x + r%:num)[%classic :> set rT. Proof. From dbb124f3e03e24723989479e30e8ef570a1d4bfc Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 27 Aug 2023 14:59:24 -0400 Subject: [PATCH 3/8] updating changelog --- CHANGELOG_UNRELEASED.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c809887ec..f8e481a26 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -40,6 +40,10 @@ + new definition `regular_space`. + new lemma `ent_closure`. +- in file `lebesgue_integral.v`, + + new lemmas `simple_bounded`, `measurable_bounded_integrable`, + `compact_finite_measure`, and `cvge_harmonic`. + ### Changed - `mnormalize` moved from `kernel.v` to `measure.v` and generalized From 0f5365368d46a6561bd1f6bbc81a783140bbb567 Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 27 Aug 2023 16:10:52 -0400 Subject: [PATCH 4/8] proving full theorem instead --- theories/lebesgue_integral.v | 148 +++++++++++++++++++++-------------- 1 file changed, 91 insertions(+), 57 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 4f5fd5087..dda6a6a13 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1761,6 +1761,7 @@ apply: le_lt_trans. by rewrite [_ eps]splitr EFinD lte_add. Qed. + End lusin. Section emeasurable_fun. @@ -4888,71 +4889,104 @@ Lemma cvge_harmonic : (EFin \o (@harmonic rT)) @ \oo --> 0%E. Proof. by apply: cvg_EFin; [exact: nearW | exact: cvg_harmonic]. Qed. Local Open Scope ereal_scope. -Local Lemma approximation_continuous_sfun (E : set R) (f : {sfun R >-> rT}): - measurable E -> mu E < +oo -> exists g_ : (rT -> rT)^nat, +Local Lemma approximation_continuous_bounded (E : set R) (f : R -> R^o): + measurable E -> mu E < +oo -> mu.-integrable E (EFin \o f) -> + exists g_ : (rT -> rT)^nat, [/\ forall n, continuous (g_ n : R -> R), forall n, mu.-integrable E (EFin \o g_ n) & (fun n => \int[mu]_(z in E) `|(f z - g_ n z)%:E|) --> 0]. Proof. -move=> mE Efin; have : (exists M, 0 < M /\ forall x, `|f x| <= M)%R. - case: (@simple_bounded _ _ _ f) => M [_ /= bdM]. +move=> mE Efin intf. +have mf : measurable_fun E f by case/integrableP:intf => /EFin_measurable_fun. +suff apxf eps : exists (h : rT -> rT), (eps > 0)%R -> + [/\ continuous h, + mu.-integrable E (EFin \o h) & + \int[mu]_(z in E) `|(f z - h z)%:E| < eps%:E]. + pose g_ (n : nat) := projT1 (cid (apxf (n.+1%:R^-1))); exists g_; split. + - by move=> n; have [] := projT2 (cid (apxf (n.+1%:R^-1))) => //. + - by move=> n; have [] := projT2 (cid (apxf (n.+1%:R^-1))) => //. + apply/cvg_ballP => eps epspos. + have /cvg_ballP/(_ eps epspos) [N _ Nball] := cvge_harmonic. + exists N => //; apply: (subset_trans Nball) => n. + rewrite /ball /= /ereal_ball contract0 ?mul0r ?sub0r ?normrN. + move/(lt_trans _); apply; rewrite ?ger0_norm; first last. + - by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0 integral_ge0. + - by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0. + have [] := projT2 (cid (apxf (n.+1%:R^-1))) => // ? ? ?. + by rewrite -lt_expandRL // ?contractK // inE contract_le1. +case epspos: (0 < eps)%R; last by exists point. +move: eps epspos => _/posnumP[eps]. +have [g [gfe2 ?]] : exists (g : {sfun R >-> rT}), + \int[mu]_(z in E) `|(f z - g z)%:E| < (eps%:num/2)%:E /\ + mu.-integrable E (EFin \o g). + have [g_ [intG ?]] := approximation_sfun_integrable mE intf. + case/fine_fcvg/cvg_ballP/(_ (eps%:num/2)) => // n _ Nb; exists (g_ n). + have ? : \int[mu]_(z in E) `|(f z - g_ n z)%:E| \is a fin_num. + apply: integral_fune_fin_num => //; apply: integrable_abse. + under eq_fun => ? do rewrite ?EFinB; apply: integrableB => //. + exact: intG. + split; last by exact: intG. + have /= := Nb _ (leqnn n); rewrite /ball /= sub0r normrN -fine_abse //. + rewrite -?lte_fin fineK ?abse_fin_num // => /(le_lt_trans _); apply. + by rewrite lee_abs. +have mg : measurable_fun E g by exact: (measurable_funS measurableT). +have [M [Mpos Mbd]] : (exists M, 0 < M /\ forall x, `|g x| <= M)%R. + case: (@simple_bounded _ _ _ g) => M [_ /= bdM]. exists (`|M| + 1)%R; split; first exact: ltr_wpDl. by move=> x; apply: bdM => //; apply: ltr_pwDr; rewrite // ler_norm. -have mf : measurable_fun E f. - apply: (measurable_funS measurableT) => // ? /= ?; rewrite setTI. -case=> M [Mpos Mbd]. -have apxf eps : exists (g : rT -> rT), (eps > 0)%R -> - [/\ continuous g, - mu.-integrable E (EFin \o g) & - \int[mu]_(z in E) `|(f z - g z)%:E| < eps%:E]. - case epspos: (0 < eps)%R; last by exists point. - move: eps epspos => _/posnumP[eps]. - have [] // := @measurable_almost_continuous rT E mE _ f (eps%:num/(M *+ 2)). - by apply: divr_gt0 => //; apply: mulrn_wgt0. - move=> A [cptA AE /= muAE ctsAF]. - have [] := continuous_bounded_extension _ _ Mpos ctsAF. - - exact: pseudometric_normal. - - by apply: compact_closed => //; exact: Rhausdorff . - - by move=> ? ?; exact: Mbd. - have mA : measurable A by exact: compact_measurable. - move=> g [fg ctsg gbdM]; have mg : measurable_fun E g. - apply: subspace_continuous_measurable_fun => //. - exact: continuous_subspaceT. - have intg : mu.-integrable E (EFin \o g). - apply: measurable_bounded_integrable => //. - exists M; split; rewrite ?num_real // => ? sx ? ? /=. - by apply: ltW; apply: (le_lt_trans _ sx); apply: gbdM. - exists g; split => //; rewrite -(setDKU AE) integral_setU => //; first last. - - by rewrite /disj_set setDKI. - - rewrite setDKU //; (do 2 (apply: measurableT_comp => //)). - exact: measurable_funB. - - exact: measurableD. - rewrite (@ae_eq_integral _ _ _ mu A (fun=> 0)) //; first last. - - by apply: aeW => z Az; rewrite (fg z) ?inE // subrr normr0. - - apply: (measurable_funS mE) => //; (do 2 (apply: measurableT_comp => //)). - exact: measurable_funB. - rewrite integral0 adde0; under eq_fun => ? do rewrite -[EFin _]gee0_abs //. - apply: le_lt_trans; first apply: (@integral_le_bound _ _ _ _ _ _ (M *+ 2)%:E). - - exact: measurableD. +have [] // := @measurable_almost_continuous rT E mE _ g (eps%:num/2/(M *+ 2)). + by apply: divr_gt0 => //; apply: mulrn_wgt0. +move=> A [cptA AE /= muAE ctsAF]. +have [] := continuous_bounded_extension _ _ Mpos ctsAF. +- exact: pseudometric_normal. +- by apply: compact_closed => //; exact: Rhausdorff . +- by move=> ? ?; exact: Mbd. +have mA : measurable A by exact: compact_measurable. +move=> h [gh ctsh hbdM]; have mh : measurable_fun E h. + apply: subspace_continuous_measurable_fun => //. + exact: continuous_subspaceT. +have intg : mu.-integrable E (EFin \o h). + apply: measurable_bounded_integrable => //. + exists M; split; rewrite ?num_real // => ? sx ? ? /=. + by apply: ltW; apply: (le_lt_trans _ sx); apply: hbdM. +exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans. +pose fgh x := (`|(f x - g x)%:E| + `|(g x - h x)%:E|). + apply (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //. - apply: (measurable_funS mE) => //; (do 2 (apply: measurableT_comp => //)). exact: measurable_funB. - - by rewrite lee_fin mulrn_wge0 //; apply: ltW. - - apply: aeW => z [Ez _]; rewrite /= normr_id lee_fin mulr2n. - apply: le_trans; first exact: ler_normB. - by apply: lerD; [exact: Mbd | exact: gbdM]. - by rewrite -lte_pdivl_mull ? mulrn_wgt0 // muleC -EFinM. -pose g_ (n : nat) := projT1 (cid (apxf (n.+1%:R^-1))); exists g_; split. -- by move=> n; have [] := projT2 (cid (apxf (n.+1%:R^-1))) => //. -- by move=> n; have [] := projT2 (cid (apxf (n.+1%:R^-1))) => //. -apply/cvg_ballP => eps epspos. -have /cvg_ballP/(_ eps epspos) [N _ Nball] := cvge_harmonic. -exists N => //; apply: (subset_trans Nball) => n. -rewrite /ball /= /ereal_ball contract0 ?mul0r ?sub0r ?normrN. -move/(lt_trans _); apply; rewrite ?ger0_norm; first last. -- by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0 integral_ge0. -- by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0. -have [] := projT2 (cid (apxf (n.+1%:R^-1))) => // ? ? ?. -by rewrite -lt_expandRL // ?contractK // inE contract_le1. + - by move=> z _; rewrite /fgh. + - rewrite /fgh; apply: measurableT_comp => //. + by apply: measurable_funD => //; + apply: (measurable_funS mE) => //; (apply: measurableT_comp => //); + exact: measurable_funB. + - move=> x _; rewrite (_ : f x - h x = (f x - g x) + (g x - h x))%R. + rewrite lee_fin ler_normD //. + by rewrite -addrA [(- _ + _)%R]addrA [(-_ + _)%R]addrC subrr sub0r. +rewrite integralD //; first last. +- apply: integrable_abse. + by under eq_fun => ? do rewrite ?EFinB; apply: integrableB => //. +- apply: integrable_abse. + by under eq_fun => ? do rewrite ?EFinB; apply: integrableB => //. +rewrite EFinD; apply: lte_add => //. +rewrite -(setDKU AE) integral_setU => //; first last. +- by rewrite /disj_set setDKI. +- rewrite setDKU //; (do 2 (apply: measurableT_comp => //)). + exact: measurable_funB. +- exact: measurableD. +rewrite (@ae_eq_integral _ _ _ mu A (fun=> 0)) //; first last. +- by apply: aeW => z Az; rewrite (gh z) ?inE // subrr abse0. +- apply: (measurable_funS mE) => //; (do 2 (apply: measurableT_comp => //)). + exact: measurable_funB. +rewrite integral0 adde0. +apply: le_lt_trans; first apply: (@integral_le_bound _ _ _ _ _ _ (M *+ 2)%:E). +- exact: measurableD. +- apply: (measurable_funS mE) => //; (apply: measurableT_comp => //). + exact: measurable_funB. +- by rewrite lee_fin mulrn_wge0 //; apply: ltW. +- apply: aeW => z [Ez _]; rewrite /= lee_fin mulr2n. + apply: le_trans; first exact: ler_normB. + by apply: lerD; [exact: Mbd | exact: hbdM]. +by rewrite -lte_pdivl_mull ? mulrn_wgt0 // muleC -EFinM. Qed. Section continuous_density_L1. From 3645271fa7a76bc59d29e5d135fb431a8db9dc5c Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 27 Aug 2023 16:12:28 -0400 Subject: [PATCH 5/8] changelog --- CHANGELOG_UNRELEASED.md | 3 ++- theories/lebesgue_integral.v | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f8e481a26..e5a447ff2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -42,7 +42,8 @@ - in file `lebesgue_integral.v`, + new lemmas `simple_bounded`, `measurable_bounded_integrable`, - `compact_finite_measure`, and `cvge_harmonic`. + `compact_finite_measure`, `approximation_continuous_integrable`, and + `cvge_harmonic`. ### Changed diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index dda6a6a13..5288e3c09 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4889,7 +4889,7 @@ Lemma cvge_harmonic : (EFin \o (@harmonic rT)) @ \oo --> 0%E. Proof. by apply: cvg_EFin; [exact: nearW | exact: cvg_harmonic]. Qed. Local Open Scope ereal_scope. -Local Lemma approximation_continuous_bounded (E : set R) (f : R -> R^o): +Local Lemma approximation_continuous_integrable (E : set R) (f : R -> R^o): measurable E -> mu E < +oo -> mu.-integrable E (EFin \o f) -> exists g_ : (rT -> rT)^nat, [/\ forall n, continuous (g_ n : R -> R), From 696afeb2ed6b8ef3b1e19b3780d64c5228bef4ee Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 28 Aug 2023 14:10:23 +0900 Subject: [PATCH 6/8] shorter simple_bouned with bigmax lemmas --- CHANGELOG_UNRELEASED.md | 9 +++++ classical/cardinality.v | 4 ++- classical/mathcomp_extra.v | 22 ++++++++++++ theories/constructive_ereal.v | 10 ++++++ theories/kernel.v | 2 +- theories/lebesgue_integral.v | 64 +++++++++++++++++------------------ 6 files changed, 76 insertions(+), 35 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e5a447ff2..a2cf03cc7 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -45,6 +45,12 @@ `compact_finite_measure`, `approximation_continuous_integrable`, and `cvge_harmonic`. +- in `mathcomp_extra.v`: + + lemmas `le_bigmax_seq`, `bigmax_sup_seq` + +- in `constructive_ereal.v`: + + lemma `bigmaxe_fin_num` + ### Changed - `mnormalize` moved from `kernel.v` to `measure.v` and generalized @@ -58,6 +64,9 @@ - removed dependency in `Rstruct.v` on `normedtype.v`: - added dependency in `normedtype.v` on `Rstruct.v`: +- in `cardinality.f`: + + implicits of `fimfunP` + ### Renamed - in `normedtype.v`: diff --git a/classical/cardinality.v b/classical/cardinality.v index 6b3bbbf1b..6e2c9a79d 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -1235,13 +1235,15 @@ HB.mixin Record FiniteImage aT rT (f : aT -> rT) := { }. HB.structure Definition FImFun aT rT := {f of @FiniteImage aT rT f}. +Arguments fimfunP {aT rT} _. +#[global] Hint Resolve fimfunP : core. + Reserved Notation "{ 'fimfun' aT >-> T }" (at level 0, format "{ 'fimfun' aT >-> T }"). Reserved Notation "[ 'fimfun' 'of' f ]" (at level 0, format "[ 'fimfun' 'of' f ]"). Notation "{ 'fimfun' aT >-> T }" := (@FImFun.type aT T) : form_scope. Notation "[ 'fimfun' 'of' f ]" := [the {fimfun _ >-> _} of f] : form_scope. -#[global] Hint Resolve fimfunP : core. Lemma fimfun_inP {aT rT} (f : {fimfun aT >-> rT}) (D : set aT) : finite_set (f @` D). diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index d3522198f..607722b63 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1416,3 +1416,25 @@ Qed. End max_min. Notation trivial := (ltac:(done)). + +Section bigmax_seq. +Context d {T : orderType d} {x : T} {I : eqType}. +Variables (r : seq I) (i0 : I) (P : pred I). + +(* NB: as of [2023-08-28], bigop.leq_bigmax_seq already exists for nat *) +Lemma le_bigmax_seq F : + i0 \in r -> P i0 -> (F i0 <= \big[Order.max/x]_(i <- r | P i) F i)%O. +Proof. +move=> + Pi0; elim: r => // h t ih; rewrite inE big_cons. +move=> /predU1P[<-|i0t]; first by rewrite Pi0 le_maxr// lexx. +by case: ifPn => Ph; [rewrite le_maxr ih// orbT|rewrite ih]. +Qed. + +(* NB: as of [2023-08-28], bigop.bigmax_sup_seq already exists for nat *) +Lemma bigmax_sup_seq (m : T) (F : I -> T) : + i0 \in r -> P i0 -> (m <= F i0)%O -> + (m <= \big[Order.max/x]_(i <- r | P i) F i)%O. +Proof. by move=> i0r Pi0 ?; apply: le_trans (le_bigmax_seq _ _ _). Qed. + +End bigmax_seq. +Arguments le_bigmax_seq {d T} x {I r} i0 P. diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 67caa0952..96a8b5c6a 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -2413,6 +2413,16 @@ Lemma mineMl z x y : z \is a fin_num -> 0 < z -> mine x y * z = mine (x * z) (y * z). Proof. by move=> zfin z0; rewrite muleC mineMr// !(muleC z). Qed. +Lemma bigmaxe_fin_num (s : seq R) r : r \in s -> + \big[maxe/-oo%E]_(i <- s) i%:E \is a fin_num. +Proof. +move=> rs; have {rs} : s != [::]. + by rewrite -size_eq0 -lt0n -has_predT; apply/hasP; exists r. +elim: s => [[]//|a l]; have [-> _ _|_ /(_ isT) ih _] := eqVneq l [::]. + by rewrite big_seq1. +by rewrite big_cons {1}/maxe; case: (_ < _)%E. +Qed. + Lemma lee_pemull x y : 0 <= y -> 1 <= x -> y <= x * y. Proof. move: x y => [x| |] [y| |] //; last by rewrite mulyy. diff --git a/theories/kernel.v b/theories/kernel.v index a91eb87c8..9047eb019 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -1006,7 +1006,7 @@ HB.instance Definition _ n := @isMeasurableFun.Build _ _ _ _ (mk_2 n). Let fk_2 n : finite_set (range (k_2 n)). Proof. -have := @fimfunP _ _ (k_ n). +have := fimfunP (k_ n). suff : range (k_ n) = range (k_2 n) by move=> <-. by apply/seteqP; split => r [y ?] <-; [exists (point, y)|exists y.2]. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 5288e3c09..fc24c780f 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -403,23 +403,19 @@ Qed. Section simple_bounded. Context d (T : measurableType d) (R : realType). -Lemma simple_bounded {f : {sfun T >-> R}} : +Lemma simple_bounded {f : {sfun T >-> R}} : bounded_fun (f : T -> [normedModType R of R^o]). Proof. -case/finite_seqP:(@fimfunP _ _ f) => r fr. -exists (fine (\big[maxe/-oo%E]_(i <- r) (`|i|)%:E)). -split; rewrite ?num_real // => x mx z _; apply: ltW; apply: (le_lt_trans _ mx). -rewrite (_ : normr (f z) = fine (EFin (normr (f z)))) // fine_le //; first last. -have fzr : (f z \in r) by (have : (range f) (f z) by exists z); rewrite fr. - by rewrite (big_rem _ fzr) /= le_maxr; apply/orP; left. -have fpr : (exists p, p \in r). - by exists (f point); (have : (range f) (f point) by exists point); rewrite fr. -elim: r fpr {fr mx}; first by case => ?. -move=> a l IH _; case: (pselect (exists p, p \in l)). - by move/IH => bfin; rewrite big_cons /maxe; case: (_ < _)%E; rewrite ?bfin. -move=> npl; suff : l == [::] by move/eqP ->; rewrite big_seq1. -rewrite -set_seq_eq0; apply/eqP; rewrite -subset0; move/forallNP: npl; apply. +have /finite_seqP[r fr] := fimfunP f. +exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)). +split; rewrite ?num_real// => x mx z _; apply/ltW/(le_lt_trans _ mx). +have ? : f z \in r by have := imageT f z; rewrite fr. +rewrite -[leLHS]/(fine `|f z|%:E) fine_le//. + have := @bigmaxe_fin_num _ (map normr r) `|f z|. + by rewrite big_map => ->//; apply/mapP; exists (f z). +by rewrite (bigmax_sup_seq _ _ (lexx _)). Qed. + End simple_bounded. Section nnsfun_functions. @@ -1654,7 +1650,7 @@ Let lusin_simple (f : {sfun R >-> rT}) (eps : rT) : (0 < eps)%R -> exists K, [/\ compact K, K `<=` A, mu (A `\` K) < eps%:E & {within K, continuous f}]. Proof. -move: eps=> _/posnumP[eps]; have [N /card_fset_set rfN] := @fimfunP _ _ f. +move: eps=> _/posnumP[eps]; have [N /card_fset_set rfN] := fimfunP f. pose Af x : set R := A `&` f @^-1` [set x]. have mAf x : measurable (Af x) by exact: measurableI. have finAf x : mu (Af x) < +oo. @@ -4765,7 +4761,7 @@ Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (E : set T) (mE : measurable E). Lemma measurable_bounded_integrable (f : T -> R^o) : - (mu E < +oo)%E -> measurable_fun E f -> + (mu E < +oo)%E -> measurable_fun E f -> [bounded f x | x in E] -> mu.-integrable E (EFin \o f). Proof. move=> Afin mfA bdA; apply/integrableP; split. @@ -4773,7 +4769,7 @@ move=> Afin mfA bdA; apply/integrableP; split. have [M [_ mrt]] := bdA; apply: le_lt_trans. apply (@integral_le_bound _ _ _ _ _ _ (`|M| + 1)%:E) => //. by apply: measurableT_comp => //; exact: subspace_continuous_measurable_fun. - by apply: aeW => z Az; rewrite lee_fin mrt // ltr_pwDr // ler_norm. + by apply: aeW => z Az; rewrite lee_fin mrt // ltr_spaddr// ler_norm. by rewrite lte_mul_pinfty. Qed. @@ -4878,7 +4874,7 @@ Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) : compact A -> {within A, continuous f} -> mu.-integrable A (EFin \o f). Proof. move=> cptA ctsfA; apply: measurable_bounded_integrable. -- exact: compact_measurable. +- exact: compact_measurable. - exact: compact_finite_measure. - by apply: subspace_continuous_measurable_fun => //; exact: compact_measurable. - have /compact_bounded [M [_ mrt]] := continuous_compact ctsfA cptA. @@ -4909,19 +4905,19 @@ suff apxf eps : exists (h : rT -> rT), (eps > 0)%R -> have /cvg_ballP/(_ eps epspos) [N _ Nball] := cvge_harmonic. exists N => //; apply: (subset_trans Nball) => n. rewrite /ball /= /ereal_ball contract0 ?mul0r ?sub0r ?normrN. - move/(lt_trans _); apply; rewrite ?ger0_norm; first last. + move/(lt_trans _); apply; rewrite ?ger0_norm; first last. - by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0 integral_ge0. - - by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0. + - by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0. have [] := projT2 (cid (apxf (n.+1%:R^-1))) => // ? ? ?. - by rewrite -lt_expandRL // ?contractK // inE contract_le1. + by rewrite -lt_expandRL // ?contractK // inE contract_le1. case epspos: (0 < eps)%R; last by exists point. move: eps epspos => _/posnumP[eps]. -have [g [gfe2 ?]] : exists (g : {sfun R >-> rT}), +have [g [gfe2 ?]] : exists (g : {sfun R >-> rT}), \int[mu]_(z in E) `|(f z - g z)%:E| < (eps%:num/2)%:E /\ mu.-integrable E (EFin \o g). have [g_ [intG ?]] := approximation_sfun_integrable mE intf. case/fine_fcvg/cvg_ballP/(_ (eps%:num/2)) => // n _ Nb; exists (g_ n). - have ? : \int[mu]_(z in E) `|(f z - g_ n z)%:E| \is a fin_num. + have ? : \int[mu]_(z in E) `|(f z - g_ n z)%:E| \is a fin_num. apply: integral_fune_fin_num => //; apply: integrable_abse. under eq_fun => ? do rewrite ?EFinB; apply: integrableB => //. exact: intG. @@ -4929,11 +4925,12 @@ have [g [gfe2 ?]] : exists (g : {sfun R >-> rT}), have /= := Nb _ (leqnn n); rewrite /ball /= sub0r normrN -fine_abse //. rewrite -?lte_fin fineK ?abse_fin_num // => /(le_lt_trans _); apply. by rewrite lee_abs. -have mg : measurable_fun E g by exact: (measurable_funS measurableT). +have mg : measurable_fun E (g : {mfun R >-> rT}(*NB(rei): shouldn't need this constraint, should we?*)). + by apply: (measurable_funS measurableT) => //; exact: measurable_funP. have [M [Mpos Mbd]] : (exists M, 0 < M /\ forall x, `|g x| <= M)%R. case: (@simple_bounded _ _ _ g) => M [_ /= bdM]. - exists (`|M| + 1)%R; split; first exact: ltr_wpDl. - by move=> x; apply: bdM => //; apply: ltr_pwDr; rewrite // ler_norm. + exists (`|M| + 1)%R; split; first exact: ltr_spaddr. + by move=> x; apply: bdM => //; apply: ltr_spaddr; rewrite // ler_norm. have [] // := @measurable_almost_continuous rT E mE _ g (eps%:num/2/(M *+ 2)). by apply: divr_gt0 => //; apply: mulrn_wgt0. move=> A [cptA AE /= muAE ctsAF]. @@ -4955,12 +4952,12 @@ pose fgh x := (`|(f x - g x)%:E| + `|(g x - h x)%:E|). - apply: (measurable_funS mE) => //; (do 2 (apply: measurableT_comp => //)). exact: measurable_funB. - by move=> z _; rewrite /fgh. - - rewrite /fgh; apply: measurableT_comp => //. + - rewrite /fgh; apply: measurableT_comp => //. by apply: measurable_funD => //; apply: (measurable_funS mE) => //; (apply: measurableT_comp => //); exact: measurable_funB. - - move=> x _; rewrite (_ : f x - h x = (f x - g x) + (g x - h x))%R. - rewrite lee_fin ler_normD //. + - move=> x _; rewrite (_ : f x - h x = (f x - g x) + (g x - h x))%R. + rewrite lee_fin ler_norm_add //. by rewrite -addrA [(- _ + _)%R]addrA [(-_ + _)%R]addrC subrr sub0r. rewrite integralD //; first last. - apply: integrable_abse. @@ -4977,18 +4974,19 @@ rewrite (@ae_eq_integral _ _ _ mu A (fun=> 0)) //; first last. - by apply: aeW => z Az; rewrite (gh z) ?inE // subrr abse0. - apply: (measurable_funS mE) => //; (do 2 (apply: measurableT_comp => //)). exact: measurable_funB. -rewrite integral0 adde0. +rewrite integral0 adde0. apply: le_lt_trans; first apply: (@integral_le_bound _ _ _ _ _ _ (M *+ 2)%:E). - exact: measurableD. - apply: (measurable_funS mE) => //; (apply: measurableT_comp => //). exact: measurable_funB. - by rewrite lee_fin mulrn_wge0 //; apply: ltW. - apply: aeW => z [Ez _]; rewrite /= lee_fin mulr2n. - apply: le_trans; first exact: ler_normB. - by apply: lerD; [exact: Mbd | exact: hbdM]. + apply: le_trans; first exact: ler_norm_sub. + by apply: ler_add; [exact: Mbd | exact: hbdM]. by rewrite -lte_pdivl_mull ? mulrn_wgt0 // muleC -EFinM. Qed. -Section continuous_density_L1. + +End continuous_density_L1. Section fubini_functions. Local Open Scope ereal_scope. From fe955b51af6a63f500da85d7f7096d97a7173f40 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 28 Aug 2023 16:42:33 +0900 Subject: [PATCH 7/8] fix, mv 1 lemma, marginally shorter scripts --- CHANGELOG_UNRELEASED.md | 11 ++- theories/lebesgue_integral.v | 173 ++++++++++++++++------------------- theories/sequences.v | 3 + 3 files changed, 89 insertions(+), 98 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a2cf03cc7..604eb9d08 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -42,8 +42,10 @@ - in file `lebesgue_integral.v`, + new lemmas `simple_bounded`, `measurable_bounded_integrable`, - `compact_finite_measure`, `approximation_continuous_integrable`, and - `cvge_harmonic`. + `compact_finite_measure`, `approximation_continuous_integrable` + +- in `sequences.v`: + + lemma `cvge_harmonic` - in `mathcomp_extra.v`: + lemmas `le_bigmax_seq`, `bigmax_sup_seq` @@ -64,9 +66,12 @@ - removed dependency in `Rstruct.v` on `normedtype.v`: - added dependency in `normedtype.v` on `Rstruct.v`: -- in `cardinality.f`: +- in `cardinality.v`: + implicits of `fimfunP` +- in `lebesgue_integral.v`: + + implicits of `integral_le_bound` + ### Renamed - in `normedtype.v`: diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index fc24c780f..7ec0326db 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -403,7 +403,7 @@ Qed. Section simple_bounded. Context d (T : measurableType d) (R : realType). -Lemma simple_bounded {f : {sfun T >-> R}} : +Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun (f : T -> [normedModType R of R^o]). Proof. have /finite_seqP[r fr] := fimfunP f. @@ -1757,7 +1757,6 @@ apply: le_lt_trans. by rewrite [_ eps]splitr EFinD lte_add. Qed. - End lusin. Section emeasurable_fun. @@ -4283,6 +4282,7 @@ by apply: ae_ge0_le_integral => //; exact: measurableT_comp. Qed. End integral_bounded. +Arguments integral_le_bound {d T R mu D f} M. Section integral_ae_eq. Local Open Scope ereal_scope. @@ -4760,21 +4760,19 @@ Section simple_density_L1. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (E : set T) (mE : measurable E). +Local Open Scope ereal_scope. + Lemma measurable_bounded_integrable (f : T -> R^o) : - (mu E < +oo)%E -> measurable_fun E f -> + mu E < +oo -> measurable_fun E f -> [bounded f x | x in E] -> mu.-integrable E (EFin \o f). Proof. -move=> Afin mfA bdA; apply/integrableP; split. - exact/EFin_measurable_fun. +move=> Afin mfA bdA; apply/integrableP; split; first exact/EFin_measurable_fun. have [M [_ mrt]] := bdA; apply: le_lt_trans. - apply (@integral_le_bound _ _ _ _ _ _ (`|M| + 1)%:E) => //. - by apply: measurableT_comp => //; exact: subspace_continuous_measurable_fun. - by apply: aeW => z Az; rewrite lee_fin mrt // ltr_spaddr// ler_norm. + apply: (integral_le_bound (`|M| + 1)%:E) => //; first exact: measurableT_comp. + by apply: aeW => z Az; rewrite lee_fin mrt// ltr_spaddr// ler_norm. by rewrite lte_mul_pinfty. Qed. -Local Open Scope ereal_scope. - Let sfun_dense_L1_pos (f : T -> \bar R) : mu.-integrable E f -> (forall x, E x -> 0 <= f x) -> exists g_ : {sfun T >-> R}^nat, @@ -4857,17 +4855,15 @@ Section continuous_density_L1. Context (rT : realType). Let mu := [the measure _ _ of @lebesgue_measure rT]. Let R := [the measurableType _ of measurableTypeR rT]. +Local Open Scope ereal_scope. -Lemma compact_finite_measure (A : set R^o) : - compact A -> (mu A < +oo)%E. +Lemma compact_finite_measure (A : set R^o) : compact A -> mu A < +oo. Proof. -move => /[dup]/compact_measurable => ?; case/compact_bounded => N [_ N1x]. -have AN1 : A `<=` `[- (`|N| + 1), `|N| + 1]. +move=> /[dup]/compact_measurable => mA /compact_bounded[N [_ N1x]]. +have AN1 : (A `<=` `[- (`|N| + 1), `|N| + 1])%R. by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_spaddr// ler_norm. -apply: le_lt_trans; first apply: (le_measure _ _ _ AN1); first exact /mem_set. - by apply/mem_set; exact: measurable_itv. -rewrite /= lebesgue_measure_itv hlength_itv /= -fun_if. -by case E : (_%:E < _%:E)%E => //=; rewrite ltry. +rewrite (le_lt_trans (le_measure _ _ _ AN1)) ?inE//=. +by rewrite lebesgue_measure_itv hlength_itv/= lte_fin gtr_opp// EFinD ltry. Qed. Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) : @@ -4877,113 +4873,100 @@ move=> cptA ctsfA; apply: measurable_bounded_integrable. - exact: compact_measurable. - exact: compact_finite_measure. - by apply: subspace_continuous_measurable_fun => //; exact: compact_measurable. -- have /compact_bounded [M [_ mrt]] := continuous_compact ctsfA cptA. +- have /compact_bounded[M [_ mrt]] := continuous_compact ctsfA cptA. by exists M; split; rewrite ?num_real // => ? ? ? ?; exact: mrt. Qed. -Lemma cvge_harmonic : (EFin \o (@harmonic rT)) @ \oo --> 0%E. -Proof. by apply: cvg_EFin; [exact: nearW | exact: cvg_harmonic]. Qed. - -Local Open Scope ereal_scope. Local Lemma approximation_continuous_integrable (E : set R) (f : R -> R^o): measurable E -> mu E < +oo -> mu.-integrable E (EFin \o f) -> exists g_ : (rT -> rT)^nat, - [/\ forall n, continuous (g_ n : R -> R), + [/\ forall n, continuous (g_ n), forall n, mu.-integrable E (EFin \o g_ n) & (fun n => \int[mu]_(z in E) `|(f z - g_ n z)%:E|) --> 0]. Proof. move=> mE Efin intf. -have mf : measurable_fun E f by case/integrableP:intf => /EFin_measurable_fun. -suff apxf eps : exists (h : rT -> rT), (eps > 0)%R -> +have mf : measurable_fun E f by case/integrableP : intf => /EFin_measurable_fun. +suff apxf eps : exists h : rT -> rT, (eps > 0)%R -> [/\ continuous h, mu.-integrable E (EFin \o h) & \int[mu]_(z in E) `|(f z - h z)%:E| < eps%:E]. - pose g_ (n : nat) := projT1 (cid (apxf (n.+1%:R^-1))); exists g_; split. - - by move=> n; have [] := projT2 (cid (apxf (n.+1%:R^-1))) => //. - - by move=> n; have [] := projT2 (cid (apxf (n.+1%:R^-1))) => //. + pose g_ n := projT1 (cid (apxf n.+1%:R^-1)); exists g_; split. + - by move=> n; have [] := projT2 (cid (apxf n.+1%:R^-1)). + - by move=> n; have [] := projT2 (cid (apxf n.+1%:R^-1)). apply/cvg_ballP => eps epspos. - have /cvg_ballP/(_ eps epspos) [N _ Nball] := cvge_harmonic. + have /cvg_ballP/(_ eps epspos)[N _ Nball] := @cvge_harmonic rT. exists N => //; apply: (subset_trans Nball) => n. - rewrite /ball /= /ereal_ball contract0 ?mul0r ?sub0r ?normrN. - move/(lt_trans _); apply; rewrite ?ger0_norm; first last. - - by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0 integral_ge0. - - by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0. - have [] := projT2 (cid (apxf (n.+1%:R^-1))) => // ? ? ?. - by rewrite -lt_expandRL // ?contractK // inE contract_le1. -case epspos: (0 < eps)%R; last by exists point. -move: eps epspos => _/posnumP[eps]. -have [g [gfe2 ?]] : exists (g : {sfun R >-> rT}), - \int[mu]_(z in E) `|(f z - g z)%:E| < (eps%:num/2)%:E /\ + rewrite /ball /= /ereal_ball contract0 !sub0r !normrN => /(lt_trans _); apply. + rewrite ?ger0_norm; first last. + - by rewrite -le_expandLR // ?inE ?normr0// expand0 integral_ge0. + - by rewrite -le_expandLR // ?inE ?normr0// expand0. + have [] := projT2 (cid (apxf n.+1%:R^-1)) => // _ _ ipaxfn. + by rewrite -lt_expandRL ?contractK// inE contract_le1. +have [|] := ltP 0%R eps; last by exists point. +move: eps => _/posnumP[eps]. +have [g [gfe2 ig]] : exists g : {sfun R >-> rT}, + \int[mu]_(z in E) `|(f z - g z)%:E| < (eps%:num / 2)%:E /\ mu.-integrable E (EFin \o g). have [g_ [intG ?]] := approximation_sfun_integrable mE intf. - case/fine_fcvg/cvg_ballP/(_ (eps%:num/2)) => // n _ Nb; exists (g_ n). - have ? : \int[mu]_(z in E) `|(f z - g_ n z)%:E| \is a fin_num. - apply: integral_fune_fin_num => //; apply: integrable_abse. - under eq_fun => ? do rewrite ?EFinB; apply: integrableB => //. - exact: intG. - split; last by exact: intG. - have /= := Nb _ (leqnn n); rewrite /ball /= sub0r normrN -fine_abse //. - rewrite -?lte_fin fineK ?abse_fin_num // => /(le_lt_trans _); apply. - by rewrite lee_abs. -have mg : measurable_fun E (g : {mfun R >-> rT}(*NB(rei): shouldn't need this constraint, should we?*)). + move/fine_fcvg/cvg_ballP/(_ (eps%:num / 2)) => -[] // n _ Nb; exists (g_ n). + have fg_fin_num : \int[mu]_(z in E) `|(f z - g_ n z)%:E| \is a fin_num. + rewrite integral_fune_fin_num// integrable_abse//. + by under eq_fun do rewrite EFinB; apply: integrableB => //; exact: intG. + split; last exact: intG. + have /= := Nb _ (leqnn n); rewrite /ball/= sub0r normrN -fine_abse// -lte_fin. + by rewrite fineK ?abse_fin_num// => /le_lt_trans; apply; exact: lee_abs. +have mg : measurable_fun E g. by apply: (measurable_funS measurableT) => //; exact: measurable_funP. -have [M [Mpos Mbd]] : (exists M, 0 < M /\ forall x, `|g x| <= M)%R. - case: (@simple_bounded _ _ _ g) => M [_ /= bdM]. - exists (`|M| + 1)%R; split; first exact: ltr_spaddr. - by move=> x; apply: bdM => //; apply: ltr_spaddr; rewrite // ler_norm. -have [] // := @measurable_almost_continuous rT E mE _ g (eps%:num/2/(M *+ 2)). - by apply: divr_gt0 => //; apply: mulrn_wgt0. +have [M Mpos Mbd] : (exists2 M, 0 < M & forall x, `|g x| <= M)%R. + have [M [_ /= bdM]] := simple_bounded g. + exists (`|M| + 1)%R; first exact: ltr_spaddr. + by move=> x; rewrite bdM// ltr_spaddr// ler_norm. +have [] // := @measurable_almost_continuous _ _ mE _ g (eps%:num / 2 / (M *+ 2)). + by rewrite divr_gt0// mulrn_wgt0. move=> A [cptA AE /= muAE ctsAF]. have [] := continuous_bounded_extension _ _ Mpos ctsAF. - exact: pseudometric_normal. -- by apply: compact_closed => //; exact: Rhausdorff . +- by apply: compact_closed => //; exact: Rhausdorff. - by move=> ? ?; exact: Mbd. -have mA : measurable A by exact: compact_measurable. +have mA : measurable A := compact_measurable cptA. move=> h [gh ctsh hbdM]; have mh : measurable_fun E h. - apply: subspace_continuous_measurable_fun => //. - exact: continuous_subspaceT. + by apply: subspace_continuous_measurable_fun=> //; exact: continuous_subspaceT. have intg : mu.-integrable E (EFin \o h). apply: measurable_bounded_integrable => //. - exists M; split; rewrite ?num_real // => ? sx ? ? /=. - by apply: ltW; apply: (le_lt_trans _ sx); apply: hbdM. + exists M; split; rewrite ?num_real // => x Mx y _ /=. + by rewrite (le_trans _ (ltW Mx)). exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans. -pose fgh x := (`|(f x - g x)%:E| + `|(g x - h x)%:E|). - apply (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //. - - apply: (measurable_funS mE) => //; (do 2 (apply: measurableT_comp => //)). + pose fgh x := `|(f x - g x)%:E| + `|(g x - h x)%:E|. + apply: (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //. + - apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //. exact: measurable_funB. - by move=> z _; rewrite /fgh. - - rewrite /fgh; apply: measurableT_comp => //. - by apply: measurable_funD => //; + - apply: measurableT_comp => //; apply: measurable_funD => //; apply: (measurable_funS mE) => //; (apply: measurableT_comp => //); exact: measurable_funB. - - move=> x _; rewrite (_ : f x - h x = (f x - g x) + (g x - h x))%R. - rewrite lee_fin ler_norm_add //. - by rewrite -addrA [(- _ + _)%R]addrA [(-_ + _)%R]addrC subrr sub0r. -rewrite integralD //; first last. -- apply: integrable_abse. - by under eq_fun => ? do rewrite ?EFinB; apply: integrableB => //. -- apply: integrable_abse. - by under eq_fun => ? do rewrite ?EFinB; apply: integrableB => //. -rewrite EFinD; apply: lte_add => //. -rewrite -(setDKU AE) integral_setU => //; first last. + - move=> x _; rewrite -(subrK (g x) (f x)) -(addrA (_ + _)%R) lee_fin. + by rewrite ler_norm_add. +rewrite integralD//; first last. +- by apply: integrable_abse; under eq_fun do rewrite EFinB; apply: integrableB. +- by apply: integrable_abse; under eq_fun do rewrite EFinB; apply: integrableB. +rewrite EFinD lte_add// -(setDKU AE) integral_setU => //; first last. - by rewrite /disj_set setDKI. -- rewrite setDKU //; (do 2 (apply: measurableT_comp => //)). +- rewrite setDKU //; do 2 apply: measurableT_comp => //. exact: measurable_funB. - exact: measurableD. -rewrite (@ae_eq_integral _ _ _ mu A (fun=> 0)) //; first last. -- by apply: aeW => z Az; rewrite (gh z) ?inE // subrr abse0. -- apply: (measurable_funS mE) => //; (do 2 (apply: measurableT_comp => //)). +rewrite (@ae_eq_integral _ _ _ mu A (cst 0)) //; first last. +- by apply: aeW => z Az; rewrite (gh z) ?inE// subrr abse0. +- apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //. exact: measurable_funB. rewrite integral0 adde0. -apply: le_lt_trans; first apply: (@integral_le_bound _ _ _ _ _ _ (M *+ 2)%:E). +apply: (le_lt_trans (integral_le_bound (M *+ 2)%:E _ _ _ _)) => //. - exact: measurableD. -- apply: (measurable_funS mE) => //; (apply: measurableT_comp => //). +- apply: (measurable_funS mE) => //; apply: measurableT_comp => //. exact: measurable_funB. -- by rewrite lee_fin mulrn_wge0 //; apply: ltW. +- by rewrite lee_fin mulrn_wge0// ltW. - apply: aeW => z [Ez _]; rewrite /= lee_fin mulr2n. - apply: le_trans; first exact: ler_norm_sub. - by apply: ler_add; [exact: Mbd | exact: hbdM]. -by rewrite -lte_pdivl_mull ? mulrn_wgt0 // muleC -EFinM. + by rewrite (le_trans (ler_norm_sub _ _))// ler_add. +by rewrite -lte_pdivl_mull ?mulrn_wgt0// muleC -EFinM. Qed. End continuous_density_L1. @@ -5624,16 +5607,16 @@ suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <= move=> intfeps; apply: le_trans. apply: (ler_pmul r20 _ (le_refl _)); first exact: fine_ge0. apply: fine_le; last apply: le_abse_integral => //. - - by rewrite abse_fin_num; exact: integral_fune_fin_num. - - by apply: integral_fune_fin_num => //; exact: integrable_abse. - - by case/integrableP: int_fx. + - by rewrite abse_fin_num integral_fune_fin_num. + - by rewrite integral_fune_fin_num// integrable_abse. + - by case/integrableP : int_fx. rewrite div1r ler_pdivr_mull ?mulrn_wgt0 // -[_ * _]/(fine (_%:E)). - by rewrite fine_le // ?integral_fune_fin_num // ?integrable_abse. + by rewrite fine_le// integral_fune_fin_num// integrable_abse. apply: le_trans. - apply: (@integral_le_bound _ _ _ _ _ (fun z => (f z - f x)%:E) eps%:E) => //. - - by case/integrableP: int_fx. - - exact: ltW. - - by apply: aeW => ? ?; rewrite /= lee_fin distrC; apply: feps. +- apply: (@integral_le_bound _ _ _ _ _ (fun z => (f z - f x)%:E) eps%:E) => //. + + by case/integrableP: int_fx. + + exact: ltW. + + by apply: aeW => ? ?; rewrite /= lee_fin distrC feps. by rewrite ritv //= -EFinM lee_fin mulrC. Unshelve. all: by end_near. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index 6e48eedff..0233ad681 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -771,6 +771,9 @@ rewrite (le_trans (ltW (archi_boundP _)))// ler_nat -add1n -leq_subLR. by near: i; apply: nbhs_infty_ge. Unshelve. all: by end_near. Qed. +Lemma cvge_harmonic {R : archiFieldType} : (EFin \o @harmonic R) @ \oo --> 0%E. +Proof. by apply: cvg_EFin; [exact: nearW | exact: cvg_harmonic]. Qed. + Lemma dvg_harmonic (R : numFieldType) : ~ cvg (series (@harmonic R)). Proof. have ge_half n : (0 < n)%N -> 2^-1 <= \sum_(n <= i < n.*2) harmonic i. From 5582231d135c2dcf005a421b11b47b3ba8173dd3 Mon Sep 17 00:00:00 2001 From: zstone Date: Wed, 30 Aug 2023 23:28:34 -0400 Subject: [PATCH 8/8] making lemma non-local --- theories/lebesgue_integral.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 7ec0326db..85e19b823 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4877,7 +4877,7 @@ move=> cptA ctsfA; apply: measurable_bounded_integrable. by exists M; split; rewrite ?num_real // => ? ? ? ?; exact: mrt. Qed. -Local Lemma approximation_continuous_integrable (E : set R) (f : R -> R^o): +Lemma approximation_continuous_integrable (E : set R) (f : R -> R^o): measurable E -> mu E < +oo -> mu.-integrable E (EFin \o f) -> exists g_ : (rT -> rT)^nat, [/\ forall n, continuous (g_ n),