From 84ff007986bd555bf6d4afdbc7d963c919666fc1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 3 Dec 2024 15:40:55 +0900 Subject: [PATCH] deprecate approximation and make its interface accessible --- CHANGELOG_UNRELEASED.md | 22 ++++ theories/charge.v | 14 +-- theories/kernel.v | 49 +++++--- theories/lebesgue_integral.v | 230 ++++++++++++++++++++--------------- theories/lebesgue_measure.v | 14 ++- 5 files changed, 200 insertions(+), 129 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index acacf8db1..a320654e4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,16 +10,38 @@ - in `normedtype.v`: + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP` +- in `lebesgue_measure.v`: + + lemma `measurable_indicP` + +- in `lebesgue_integral.v`: + + definition `approx_A` (was `Let A`) + + definition `approx_B` (was `Let B`) + + lemma `measurable_fun_sum` + + lemma `integrable_indic` + ### Changed + +- in `lebesgue_integrale.v` + + change implicits of `measurable_funP` ### Renamed +- in `lebesgue_measure.v`: + + `measurable_fun_indic` -> `measurable_indic` + ### Generalized ### Deprecated +- in file `lebesgue_integral.v`: + + lemma `approximation` + ### Removed +- in `lebesgue_integral.v`: + + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`) + + notation `measurable_fun_indic` (deprecation since 0.6.3) + ### Infrastructure ### Misc diff --git a/theories/charge.v b/theories/charge.v index d3329dce9..1cb0670df 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1921,29 +1921,29 @@ Lemma change_of_variables f E : (forall x, 0 <= f x) -> \int[mu]_(x in E) (f x * ('d nu '/d mu) x) = \int[nu]_(x in E) f x. Proof. move=> f0 mE mf; set g := 'd nu '/d mu. -have [h [ndh hf]] := approximation mE mf (fun x _ => f0 x). +pose h := nnsfun_approx mE mf. have -> : \int[nu]_(x in E) f x = lim (\int[nu]_(x in E) (EFin \o h n) x @[n --> \oo]). have fE x : E x -> f x = lim ((EFin \o h n) x @[n --> \oo]). - by move=> Ex; apply/esym/cvg_lim => //; exact: hf. + by move=> Ex; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. under eq_integral => x /[!inE] /fE -> //. apply: monotone_convergence => //. - move=> n; apply/measurable_EFinP. by apply: (measurable_funS measurableT) => //; exact/measurable_funP. - by move=> n x Ex //=; rewrite lee_fin. - - by move=> x Ex a b /ndh /=; rewrite lee_fin => /lefP. + - by move=> x Ex a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. have -> : \int[mu]_(x in E) (f \* g) x = lim (\int[mu]_(x in E) ((EFin \o h n) \* g) x @[n --> \oo]). have fg x :E x -> f x * g x = lim (((EFin \o h n) \* g) x @[n --> \oo]). by move=> Ex; apply/esym/cvg_lim => //; apply: cvgeMr; - [exact: f_fin_num|exact: hf]. + [exact: f_fin_num|exact: cvg_nnsfun_approx]. under eq_integral => x /[!inE] /fg -> //. apply: monotone_convergence => [//| | |]. - move=> n; apply/emeasurable_funM; apply/measurable_funTS. exact/measurable_EFinP. exact: measurable_int (f_integrable _). - by move=> n x Ex //=; rewrite mule_ge0 ?lee_fin//=; exact: f_ge0. - - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin// f_ge0. + - by move=> x Ex a b ab/=; rewrite lee_wpmul2r ?lee_fin ?f_ge0//; exact/lefP/nd_nnsfun_approx. suff suf n : \int[mu]_(x in E) ((EFin \o h n) x * g x) = \int[nu]_(x in E) (EFin \o h n) x. by under eq_fun do rewrite suf. @@ -2008,7 +2008,7 @@ Proof. move=> numu mula mE; have nula := measure_dominates_trans numu mula. have mf : measurable_fun E ('d nu '/d mu). exact/measurable_funTS/(measurable_int _ (f_integrable _)). -have [h [ndh hf]] := approximation mE mf (fun x _ => f_ge0 numu x). +pose h := approximation mE mf. apply: integral_ae_eq => //. - apply: (integrableS measurableT) => //. apply: f_integrable. @@ -2018,7 +2018,7 @@ apply: integral_ae_eq => //. - move=> A AE mA; rewrite change_of_variables//. + by rewrite -!f_integral. + exact: f_ge0. - + exact: measurable_funS mf. + + by move: (mf); exact: measurable_funS. Qed. End chain_rule. diff --git a/theories/kernel.v b/theories/kernel.v index 4d154d267..6120babd7 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -571,24 +571,30 @@ Lemma measurable_fun_integral_finite_kernel (l : R.-fker X ~> Y) (k0 : forall z, 0 <= k z) (mk : measurable_fun [set: X * Y] k) : measurable_fun [set: X] (fun x => \int[l x]_y k (x, y)). Proof. -have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). -apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r. -have [l_ hl_] := measure_uub l. -by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. +pose k_ := nnsfun_approx measurableT mk. +apply: (@measurable_fun_xsection_integral _ k_). +- by move=> a b ab; exact/nd_nnsfun_approx. +- by move=> z; exact/cvg_nnsfun_approx. +- move => n r. + have [l_ hl_] := measure_uub l. + by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. Qed. Lemma measurable_fun_integral_sfinite_kernel (l : R.-sfker X ~> Y) (k0 : forall t, 0 <= k t) (mk : measurable_fun [set: X * Y] k) : measurable_fun [set: X] (fun x => \int[l x]_y k (x, y)). Proof. -have [k_ [ndk_ k_k]] := approximation measurableT mk (fun xy _ => k0 xy). -apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r. -have [l_ hl_] := sfinite_kernel l. -rewrite (_ : (fun x => _) = (fun x => - mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first. - by apply/funext => x; rewrite hl_//; exact/measurable_xsection. -apply: ge0_emeasurable_fun_sum => // m _. -by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. +pose k_ := nnsfun_approx measurableT mk. +apply: (@measurable_fun_xsection_integral _ k_). +- by move=> a b ab; exact/nd_nnsfun_approx. +- by move=> z; exact/cvg_nnsfun_approx. +- move => n r. + have [l_ hl_] := sfinite_kernel l. + rewrite (_ : (fun x => _) = (fun x => + mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first. + by apply/funext => x; rewrite hl_//; exact/measurable_xsection. + apply: ge0_emeasurable_fun_sum => // m _. + by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. Qed. End measurable_fun_integral_finite_sfinite. @@ -1007,8 +1013,11 @@ Lemma measurable_fun_integral_kernel (k : Y -> \bar R) (k0 : forall z, 0 <= k z) (mk : measurable_fun [set: Y] k) : measurable_fun [set: X] (fun x => \int[l x]_y k y). Proof. -have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). -by apply: (measurable_fun_preimage_integral ndk_ k_k) => n r; exact/ml. +pose k_ := nnsfun_approx measurableT mk. +apply: (@measurable_fun_preimage_integral _ _ _ _ _ _ k_) => //. +- by move=> a b ab; exact/nd_nnsfun_approx. +- by move=> z _; exact/cvg_nnsfun_approx. +- by move=> n r; exact/ml. Qed. End measurable_fun_integral_kernel. @@ -1077,13 +1086,13 @@ Lemma integral_kcomp x f : (forall z, 0 <= f z) -> measurable_fun [set: Z] f -> \int[kcomp l k x]_z f z = \int[l x]_y (\int[k (x, y)]_z f z). Proof. move=> f0 mf. -have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z). +pose f_ := nnsfun_approx measurableT mf. transitivity (\int[kcomp l k x]_z (lim ((f_ n z)%:E @[n --> \oo]))). - by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: f_f. + by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: cvg_nnsfun_approx. rewrite monotone_convergence//; last 3 first. by move=> n; exact/measurable_EFinP. by move=> n z _; rewrite lee_fin. - by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin. + by move=> z _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. rewrite (_ : (fun _ => _) = (fun n => \int[l x]_y (\int[k (x, y)]_z (f_ n z)%:E)))//; last first. by apply/funext => n; rewrite integral_kcomp_nnsfun. @@ -1099,12 +1108,12 @@ transitivity (\int[l x]_y lim ((\int[k (x, y)]_z (f_ n z)%:E) @[n --> \oo])). + exact/measurable_EFinP. + by move=> z _; rewrite lee_fin. + exact/measurable_EFinP. - + by move: ab => /ndf_ /lefP ab z _; rewrite lee_fin. + + by move=> z _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. apply: eq_integral => y _; rewrite -monotone_convergence//; last 3 first. - by move=> n; exact/measurable_EFinP. - by move=> n z _; rewrite lee_fin. - - by move=> z _ a b /ndf_ /lefP; rewrite lee_fin. -by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f. + - by move=> z _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. +by apply: eq_integral => z _; apply/cvg_lim => //; exact: cvg_nnsfun_approx. Qed. End integral_kcomp. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index c9b2bbfaf..88145c244 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -53,6 +53,9 @@ From mathcomp Require Import lebesgue_measure numfun realfun function_spaces. (* `[(k%:R * 2 ^- n), (k.+1%:R * 2 ^- n)[ *) (* approx D f == nondecreasing sequence of functions that *) (* approximates f over D using dyadic intervals *) +(* It uses the sets approx_A and approx_B. *) +(* nnsfun_approx D f == same as approx D f but as a nnsfun *) +(* approximates f over D using dyadic intervals *) (* Rintegral mu D f := fine (\int[mu]_(x in D) f x). *) (* mu.-integrable D f == f is measurable over D and the integral of f *) (* w.r.t. D is < +oo *) @@ -121,6 +124,7 @@ HB.mixin Record isMeasurableFun d d' (aT : sigmaRingType d) (rT : sigmaRingType }. HB.structure Definition MeasurableFun d d' aT rT := {f of @isMeasurableFun d d' aT rT f}. +Arguments measurable_funP {d d' aT rT} s. (* #[global] Hint Resolve fimfun_inP : core. *) @@ -223,7 +227,7 @@ HB.instance Definition _ x := isMeasurableFun.Build d _ aT rT (cst x) End mfun. Section mfun_realType. -Context {d} {aT : sigmaRingType d} {rT : realType}. +Context {rT : realType}. HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT (@normr rT rT) (@normr_measurable rT setT). @@ -288,7 +292,7 @@ Lemma mindicE (D : set aT) (mD : measurable D) : Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ aT rT (mindic mD) - (@measurable_fun_indic _ aT rT setT D mD). + (@measurable_indic _ aT rT setT D mD). Definition indic_mfun (D : set aT) (mD : measurable D) := [the {mfun aT >-> rT} of mindic mD]. @@ -305,17 +309,9 @@ Definition max_mfun f g := [the {mfun aT >-> _} of f \max g]. End ring. Arguments indic_mfun {d aT rT} _. - -Lemma measurable_indic d (T : measurableType d) (R : realType) - (D A : set T) : measurable A -> - measurable_fun D (\1_A : T -> R). -Proof. -by move=> mA; apply/measurable_funTS; rewrite (_ : \1__ = mindic R mA). -Qed. +(* TODO: move earlier?*) #[global] Hint Extern 0 (measurable_fun _ (\1__ : _ -> _)) => (exact: measurable_indic ) : core. -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_indic` instead")] -Notation measurable_fun_indic := measurable_indic (only parsing). Section sfun_pred. Context {d} {aT : sigmaRingType d} {rT : realType}. @@ -1033,7 +1029,7 @@ apply/eqP; rewrite eq_le; apply/andP; split. by apply: ereal_sup_ubound => /=; exists h. Qed. -Local Notation "\int_ ( x 'in' D ) F" := (integral mu D (fun x => F)) +Local Notation "\int_ ( x 'in' D ) F" := (integral mu D (fun x => F)%E) (at level 36, F at level 36, x, D at level 50, format "'[' \int_ ( x 'in' D ) '/ ' F ']'"). @@ -1086,9 +1082,9 @@ Qed. End integral. Notation "\int [ mu ]_ ( x 'in' D ) f" := - (integral mu D (fun x => f)) : ereal_scope. + (integral mu D (fun x => f)%E) : ereal_scope. Notation "\int [ mu ]_ x f" := - ((integral mu setT (fun x => f)))%E : ereal_scope. + ((integral mu setT (fun x => f)%E))%E : ereal_scope. Arguments eq_integral {d T R mu D} g. Section eq_measure_integral. @@ -1303,10 +1299,13 @@ Variables (f : T -> \bar R) (mf : measurable_fun D f). Local Notation I := (@dyadic_itv R). -Let A n k := if (k < n * 2 ^ n)%N then +Definition approx_A n k := if (k < n * 2 ^ n)%N then D `&` [set x | f x \in EFin @` [set` I n k]] else set0. -Let B n := D `&` [set x | n%:R%:E <= f x]%E. +Definition approx_B n := D `&` [set x | n%:R%:E <= f x]%E. + +Local Notation A := approx_A. +Local Notation B := approx_B. Definition approx : (T -> R)^nat := fun n x => \sum_(k < n * 2 ^ n) k%:R * 2 ^- n * \1_(A n k) x + n%:R * \1_(B n) x. @@ -1608,6 +1607,7 @@ move=> m n mn; rewrite (nnsfun_approxE n) (nnsfun_approxE m). exact: nd_approx. Qed. +#[deprecated(since="mathcomp-analysis 1.8.0", note="use `nnsfun_approx`, `cvg_nnsfun_approx`, and `nd_nnsfun_approx` instead")] Lemma approximation : (forall t, D t -> (0 <= f t)%E) -> exists g : {nnsfun T >-> R}^nat, nondecreasing_seq (g : (T -> R)^nat) /\ (forall x, D x -> EFin \o g^~ x @ \oo --> f x). @@ -1635,21 +1635,21 @@ rewrite integral_mkcond erestrict_scale [in RHS]integral_mkcond => k0. set h1 := f1 \_ D. have h10 x : 0 <= h1 x by apply: erestrict_ge0. have mh1 : measurable_fun setT h1 by exact/(measurable_restrictT _ _).1. -have [g [nd_g gh1]] := approximation measurableT mh1 (fun x _ => h10 x). +pose g := nnsfun_approx measurableT mh1. pose kg := fun n => scale_nnsfun (g n) k0. rewrite (@nd_ge0_integral_lim _ _ _ mu (fun x => k%:E * h1 x) kg). - rewrite (_ : _ \o _ = fun n => sintegral mu (scale_nnsfun (g n) k0))//. rewrite (_ : (fun _ => _) = (fun n => k%:E * sintegral mu (g n))). rewrite limeMl //; last first. - by apply: is_cvg_sintegral => // x m n mn; apply/(lef_at x nd_g). - by rewrite -(nd_ge0_integral_lim mu h10) // => x; - [exact/(lef_at x nd_g)|exact: gh1]. + by apply: is_cvg_sintegral => // x m n mn; exact/lefP/nd_nnsfun_approx. + by rewrite -(nd_ge0_integral_lim mu h10)// => [x m n mn|x]; + [exact/lefP/nd_nnsfun_approx|exact: cvg_nnsfun_approx]. by under eq_fun do rewrite (sintegralrM mu k (g _)). - by move=> t; rewrite mule_ge0. -- by move=> x m n mn; rewrite /kg ler_pM//; exact/lefP/nd_g. +- by move=> x m n mn; rewrite /kg ler_pM//; exact/lefP/nd_nnsfun_approx. - move=> x. rewrite [X in X @ \oo --> _](_ : _ = (fun n => k%:E * (g n x)%:E)) ?funeqE//. - by apply: cvgeMl => //; exact: gh1. + by apply: cvgeMl => //; exact: cvg_nnsfun_approx. Qed. End ge0_linearityZ. @@ -1677,29 +1677,28 @@ have h10 x : 0 <= h1 x by apply: erestrict_ge0. have h20 x : 0 <= h2 x by apply: erestrict_ge0. have mh1 : measurable_fun setT h1 by exact/(measurable_restrictT _ _).1. have mh2 : measurable_fun setT h2 by exact/(measurable_restrictT _ _).1. -have [g1 [nd_g1 gh1]] := approximation measurableT mh1 (fun x _ => h10 x). -have [g2 [nd_g2 gh2]] := approximation measurableT mh2 (fun x _ => h20 x). +pose g1 := nnsfun_approx measurableT mh1. +pose g2 := nnsfun_approx measurableT mh2. pose g12 := fun n => add_nnsfun (g1 n) (g2 n). rewrite (@nd_ge0_integral_lim _ _ _ mu _ g12) //; last 3 first. - by move=> x; rewrite adde_ge0. - - by apply: nondecreasing_seqD => // x; - [exact/(lef_at x nd_g1)|exact/(lef_at x nd_g2)]. + - by apply: nondecreasing_seqD => // x m n mn; + [exact/lefP/nd_nnsfun_approx|exact/lefP/nd_nnsfun_approx]. - move=> x; rewrite (_ : _ \o _ = (fun n => (g1 n x)%:E + (g2 n x)%:E))//. - apply: cvgeD => //; [|exact: gh1|exact: gh2]. + apply: cvgeD => //; [|exact: cvg_nnsfun_approx..]. by apply: ge0_adde_def => //; rewrite !inE; [exact: h10|exact: h20]. under [_ \o _]eq_fun do rewrite sintegralD. -rewrite (nd_ge0_integral_lim _ _ (fun x => lef_at x nd_g1)) //; last first. - by move=> x; exact: gh1. -rewrite (nd_ge0_integral_lim _ _ (fun x => lef_at x nd_g2)) //; last first. - by move=> x; exact: gh2. -rewrite limeD //. - by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g1). - by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g2). -rewrite ge0_adde_def => //; rewrite inE; apply: lime_ge. -- by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g1). -- by apply: nearW => n; exact: sintegral_ge0. -- by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g2). -- by apply: nearW => n; exact: sintegral_ge0. +rewrite (@nd_ge0_integral_lim _ _ _ _ _ g1)//; last 2 first. + by move=> x m n mn; exact/lefP/nd_nnsfun_approx. + by move=> x; exact/cvg_nnsfun_approx. +rewrite (@nd_ge0_integral_lim _ _ _ _ _ g2)//; last 2 first. + by move=> x m n mn; exact/lefP/nd_nnsfun_approx. + by move=> x; exact/cvg_nnsfun_approx. +rewrite limeD//; [ + by apply: is_cvg_sintegral => // x m n mn; exact/lefP/nd_nnsfun_approx..|]. +by rewrite ge0_adde_def => //; rewrite inE; apply: lime_ge; solve[ + (by apply: is_cvg_sintegral => // x m n mn; exact/lefP/nd_nnsfun_approx) || + (by apply: nearW => n; exact: sintegral_ge0)]. Qed. Lemma ge0_le_integral : (forall x, D x -> f1 x <= f2 x) -> @@ -1712,24 +1711,24 @@ have h20 x : 0 <= h2 x by apply: erestrict_ge0. have mh1 : measurable_fun setT h1 by exact/(measurable_restrictT _ _).1. have mh2 : measurable_fun setT h2 by exact/(measurable_restrictT _ _).1. have h12 x : h1 x <= h2 x by apply: lee_restrict. -have [g1 [nd_g1 /(_ _ Logic.I) gh1]] := - approximation measurableT mh1 (fun x _ => h10 _). -rewrite (nd_ge0_integral_lim _ h10 (fun x => lef_at x nd_g1) gh1)//. +pose g1 := nnsfun_approx measurableT mh1. +rewrite (@nd_ge0_integral_lim _ _ _ _ _ g1)//; last 2 first. + by move=> x m n mn; exact/lefP/nd_nnsfun_approx. + by move=> x; exact: cvg_nnsfun_approx. apply: lime_le. - by apply: is_cvg_sintegral => // t Dt; exact/(lef_at t nd_g1). + by apply: is_cvg_sintegral => // t m n mn; exact/lefP/nd_nnsfun_approx. near=> n; rewrite ge0_integralTE//; apply: ereal_sup_ubound => /=. -exists (g1 n) => // t; rewrite (le_trans _ (h12 _)) //. -have := gh1 t. +exists (g1 n) => // t; rewrite (le_trans _ (h12 _))//. have := leey (h1 t); rewrite le_eqVlt => /predU1P[->|ftoo]. by rewrite leey. have h1tfin : h1 t \is a fin_num. by rewrite fin_numE gt_eqF/= ?lt_eqF// (lt_le_trans _ (h10 t)). -have := gh1 t. +have /= := @cvg_nnsfun_approx _ _ _ _ measurableT _ mh1 (fun x _ => h10 x) t Logic.I. rewrite -(fineK h1tfin) => /fine_cvgP[ft_near]. -set u_ := (X in X --> _) => u_h1 g1h1. +set u_ := (X in X --> _) => u_h1. have <- : lim u_ = fine (h1 t) by exact/cvg_lim. rewrite lee_fin; apply: nondecreasing_cvgn_le. - by move=> // a b ab; rewrite /u_ /=; exact/lefP/nd_g1. + by move=> // a b ab; rewrite /u_ /=; exact/lefP/nd_nnsfun_approx. by apply/cvg_ex; eexists; exact: u_h1. Unshelve. all: by end_near. Qed. @@ -1751,16 +1750,14 @@ HB.instance Definition _ x : @NonNegFun T R (cst x%:num) := Lemma approximation_sfun : exists g : {sfun T >-> R}^nat, (forall x, D x -> EFin \o g ^~ x @ \oo --> f x). Proof. -have [fp_ [fp_nd fp_cvg]] := - approximation mD (measurable_funepos mf) (fun=> ltac:(by [])). -have [fn_ [fn_nd fn_cvg]] := - approximation mD (measurable_funeneg mf) (fun=> ltac:(by [])). +pose fp_ := nnsfun_approx mD (measurable_funepos mf). +pose fn_ := nnsfun_approx mD (measurable_funeneg mf). exists (fun n => [the {sfun T >-> R} of fp_ n \+ cst (-1) \* fn_ n]) => x /=. rewrite [X in X @ \oo --> _](_ : _ = EFin \o fp_^~ x \+ (-%E \o EFin \o fn_^~ x))%E; last first. by apply/funext => n/=; rewrite EFinD mulN1r. by move=> Dx; rewrite (funeposneg f); apply: cvgeD; - [exact: add_def_funeposneg|apply: fp_cvg|apply:cvgeN; exact: fn_cvg]. + [exact: add_def_funeposneg|apply: cvg_nnsfun_approx|apply:cvgeN; apply: cvg_nnsfun_approx]. Qed. End approximation_sfun. @@ -2046,6 +2043,22 @@ Proof. by move=> mf; exact/(emeasurable_funM _ mf). Qed. End emeasurable_fun. +Section measurable_fun. +Context d (T : measurableType d) (R : realType). +Implicit Types (D : set T) (f g : T -> R). + +Lemma measurable_fun_sum D I s (h : I -> (T -> R)) : + (forall n, measurable_fun D (h n)) -> + measurable_fun D (fun x => \sum_(i <- s) h i x). +Proof. +move=> mh; apply/measurable_EFinP. +rewrite (_ : _ \o _ = (fun t => \sum_(i <- s) (h i t)%:E)); last first. + by apply/funext => t/=; rewrite -sumEFin. +by apply/emeasurable_fun_sum => i; exact/measurable_EFinP. +Qed. + +End measurable_fun. + Section measurable_fun_measurable2. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). @@ -2387,13 +2400,14 @@ Section integral_indic. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D). +Implicit Type A : set T. Import HBNNSimple. -Lemma integral_indic (E : set T) : measurable E -> - \int[mu]_(x in D) (\1_E x)%:E = mu (E `&` D). +Lemma integral_indic A : measurable A -> + \int[mu]_(x in D) (\1_A x)%:E = mu (A `&` D). Proof. -move=> mE; rewrite (_ : \1_E = indic_nnsfun R mE)// integral_nnsfun//=. +move=> mA; rewrite (_ : \1_A = indic_nnsfun R mA)// integral_nnsfun//=. by rewrite restrict_indic sintegral_indic//; exact: measurableI. Qed. @@ -2474,20 +2488,20 @@ Lemma ge0_integral_mscale (mf : measurable_fun D f) : (forall x, D x -> 0 <= f x) -> \int[mscale k m]_(x in D) f x = k%:num%:E * \int[m]_(x in D) f x. Proof. -move=> f0; have [f_ [ndf_ f_f]] := approximation mD mf f0. +move=> f0; pose f_ := nnsfun_approx mD mf. transitivity (limn (fun n => \int[mscale k m]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//=. - - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //=; exact: f_f. + - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //=; exact: cvg_nnsfun_approx. - by move=> n; apply: measurableT_comp => //; exact: measurable_funTS. - by move=> n x _; rewrite lee_fin. - - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin. + - by move=> x _ a b ab; rewrite lee_fin//; exact/lefP/nd_nnsfun_approx. rewrite (_ : \int[m]_(x in D) _ = limn (fun n => \int[m]_(x in D) (f_ n x)%:E)); last first. rewrite -monotone_convergence//=. - - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //; exact: f_f. + - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. - by move=> n; exact/measurable_EFinP/measurable_funTS. - by move=> n x _; rewrite lee_fin. - - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin. + - by move=> x _ a b ab; rewrite lee_fin//; exact/lefP/nd_nnsfun_approx. rewrite -limeMl//. by congr (limn _); apply/funext => n /=; rewrite integral_mscale_nnsfun. apply/ereal_nondecreasing_is_cvgn => a b ab; apply: ge0_le_integral => //. @@ -2495,7 +2509,7 @@ apply/ereal_nondecreasing_is_cvgn => a b ab; apply: ge0_le_integral => //. - exact/measurable_EFinP/measurable_funTS. - by move=> x _; rewrite lee_fin. - exact/measurable_EFinP/measurable_funTS. -- by move=> x _; rewrite lee_fin; move/ndf_ : ab => /lefP. +- by move=> x _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. End integral_mscale. @@ -2644,19 +2658,19 @@ Lemma ge0_integral_pushforward (f : Y -> \bar R) : \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x. Proof. move=> mf f0. -have [f_ [ndf_ f_f]] := approximation measurableT mf (fun t _ => f0 t). +pose f_ := nnsfun_approx measurableT mf. transitivity (limn (fun n => \int[pushforward mu mphi]_x (f_ n x)%:E)). rewrite -monotone_convergence//. - - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: f_f. + - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. - by move=> n; exact/measurable_EFinP. - by move=> n y _; rewrite lee_fin. - - by move=> y _ m n mn; rewrite lee_fin; apply/lefP/ndf_. + - by move=> y _ m n mn; rewrite lee_fin; apply/lefP/nd_nnsfun_approx. rewrite (_ : (fun _ => _) = (fun n => \int[mu]_x (EFin \o f_ n \o phi) x)). rewrite -monotone_convergence//; last 3 first. - by move=> n /=; apply: measurableT_comp => //; exact: measurableT_comp. - by move=> n x _ /=; rewrite lee_fin. - - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_. - by apply: eq_integral => x _ /=; apply/cvg_lim => //; exact: f_f. + - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => x _ /=; apply/cvg_lim => //; exact: cvg_nnsfun_approx. apply/funext => n. have mfnphi r : measurable (f_ n @^-1` [set r] \o phi). rewrite -[_ \o _]/(phi @^-1` (f_ n @^-1` [set r])) -(setTI (_ @^-1` _)). @@ -2690,16 +2704,15 @@ Let ge0_integral_dirac (f : T -> \bar R) (mf : measurable_fun D f) (f0 : forall x, D x -> 0 <= f x) : D a -> \int[\d_a]_(x in D) (f x) = f a. Proof. -move=> Da; have [f_ [ndf_ f_f]] := approximation mD mf f0. +move=> Da; pose f_ := nnsfun_approx mD mf. transitivity (limn (fun n => \int[\d_ a]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//. - - apply: eq_integral => x Dx; apply/esym/cvg_lim => //; apply: f_f. - by rewrite inE in Dx. + - by apply: eq_integral => x /set_mem Dx; apply/esym/cvg_lim => //; apply: cvg_nnsfun_approx. - by move=> n; apply/measurable_EFinP; exact/measurable_funTS. - by move=> *; rewrite lee_fin. - - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_. + - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. rewrite (_ : (fun _ => _) = (fun n => (f_ n a)%:E)). - by apply/cvg_lim => //; exact: f_f. + by apply/cvg_lim => //; exact: cvg_nnsfun_approx. apply/funext => n. under eq_integral do rewrite fimfunE// -fsumEFin//. rewrite ge0_integral_fsum//. @@ -2803,8 +2816,7 @@ Lemma ge0_integral_measure_sum (D : set T) (mD : measurable D) (forall x, D x -> 0 <= f x) -> measurable_fun D f -> forall N, \int[msum m_ N]_(x in D) f x = \sum_(n < N) \int[m_ n]_(x in D) f x. Proof. -move=> f0 mf. -have [f_ [f_nd f_f]] := approximation mD mf f0. +move=> f0 mf; pose f_ := nnsfun_approx mD mf. elim => [|N ih]; first by rewrite big_ord0 msum_mzero integral_measure_zero. rewrite big_ord_recr/= -ih. rewrite (_ : _ m_ N.+1 = measure_add (msum m_ N) (m_ N)); last first. @@ -2816,12 +2828,12 @@ have cvg_f_ (m : {measure set T -> \bar R}) : cvgn (fun x => \int[m]_(x0 in D) (f_ x x0)%:E). apply: ereal_nondecreasing_is_cvgn => a b ab. apply: ge0_le_integral => //; [exact: f_ge0|exact: f_ge0|]. - by move=> t Dt; rewrite lee_fin; apply/lefP/f_nd. + by move=> t Dt; rewrite lee_fin; apply/lefP/nd_nnsfun_approx. transitivity (limn (fun n => \int[measure_add (msum m_ N) (m_ N)]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//; last first. - by move=> t Dt a b ab; rewrite lee_fin; exact/lefP/f_nd. - by apply: eq_integral => t /[!inE] Dt; apply/esym/cvg_lim => //; exact: f_f. + by move=> t Dt a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => t /[!inE] Dt; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. transitivity (limn (fun n => \int[msum m_ N]_(x in D) (f_ n x)%:E + \int[m_ N]_(x in D) (f_ n x)%:E)). by congr (limn _); apply/funext => n; by rewrite integral_measure_add_nnsfun. @@ -2829,8 +2841,8 @@ rewrite limeD//; do?[exact: cvg_f_]; last first. by apply: ge0_adde_def; rewrite inE; apply: lime_ge => //; do?[exact: cvg_f_]; apply: nearW => n; apply: integral_ge0 => //; exact: f_ge0. by congr (_ + _); (rewrite -monotone_convergence//; [ - apply: eq_integral => t /[!inE] Dt; apply/cvg_lim => //; exact: f_f | - move=> t Dt a b ab; rewrite lee_fin; exact/lefP/f_nd]). + apply: eq_integral => t /[!inE] Dt; apply/cvg_lim => //; exact: cvg_nnsfun_approx | + move=> t Dt a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx]). Qed. End integral_mfun_measure_sum. @@ -3045,9 +3057,9 @@ Definition Rintegral (D : set T) (f : T -> R) := End Rintegral. Notation "\int [ mu ]_ ( x 'in' D ) f" := - (Rintegral mu D (fun x => f)) : ring_scope. + (Rintegral mu D (fun x => f)%R) : ring_scope. Notation "\int [ mu ]_ x f" := - (Rintegral mu setT (fun x => f)) : ring_scope. + (Rintegral mu setT (fun x => f)%R) : ring_scope. HB.lock Definition integrable {d} {T : measurableType d} {R : realType} (mu : set T -> \bar R) D f := @@ -3280,6 +3292,24 @@ End integrable_theory. Notation "mu .-integrable" := (integrable mu) : type_scope. Arguments eq_integrable {d T R mu D} mD f. +Section integrable_theory_finite_measure. +Context {R : realType} d (T : measurableType d). +Variable mu : {finite_measure set T -> \bar R}. +Local Open Scope ereal_scope. + +Lemma integrable_indic A : measurable A -> + mu.-integrable [set: T] (fun x : T => (\1_A x)%:E). +Proof. +move=> mA; apply/integrableP; split; first exact/measurable_EFinP. +rewrite (eq_integral (fun x => (\1_A x)%:E)); last first. + by move=> t _; rewrite gee0_abs// lee_fin. +rewrite integral_indic// setIT. +rewrite (@le_lt_trans _ _ (mu setT)) ?le_measure ?inE//. +by rewrite ?ltry ?fin_num_fun_lty//; exact: fin_num_measure. +Qed. + +End integrable_theory_finite_measure. + Section sequence_measure. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). @@ -3296,7 +3326,7 @@ Proof. move=> fi mf fmoo fpoo; rewrite integralE. rewrite ge0_integral_measure_series//; last exact/measurable_funepos. rewrite ge0_integral_measure_series//; last exact/measurable_funeneg. -transitivity (\sum_(n n _; rewrite fineK//; [exact: integrable_pos_fin_num|exact: integrable_neg_fin_num]. @@ -5514,49 +5544,49 @@ Let G_ (g : {nnsfun T >-> R}^nat) n y := \int[m1]_x (g n (x, y))%:E. Lemma measurable_fun_fubini_tonelli_F : measurable_fun setT F. Proof. -have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). +pose g := nnsfun_approx measurableT mf. apply: (emeasurable_fun_cvg (F_ g)) => //. - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_F. - move=> x _. rewrite /F_ /F /fubini_F [in X in _ --> X](_ : (fun _ => _) = fun y => limn (EFin \o g ^~ (x, y))); last first. - by rewrite funeqE => y; apply/esym/cvg_lim => //; exact: g_f. + by rewrite funeqE => y; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. apply: cvg_monotone_convergence => //. - by move=> n; apply/measurable_EFinP => //; exact/measurableT_comp. - by move=> n y _; rewrite lee_fin//; exact: fun_ge0. - - by move=> y _ a b ab; rewrite lee_fin; exact/lefP/g_nd. + - by move=> y _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. Lemma measurable_fun_fubini_tonelli_G : measurable_fun setT G. Proof. -have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). +pose g := nnsfun_approx measurableT mf. apply: (emeasurable_fun_cvg (G_ g)) => //. - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_G. - move=> y _; rewrite /G_ /G /fubini_G [in X in _ --> X](_ : (fun _ => _) = fun x => limn (EFin \o g ^~ (x, y))); last first. - by rewrite funeqE => x; apply/esym/cvg_lim => //; exact: g_f. + by rewrite funeqE => x; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. apply: cvg_monotone_convergence => //. - by move=> n; apply/measurable_EFinP => //; exact/measurableT_comp. - by move=> n x _; rewrite lee_fin; exact: fun_ge0. - - by move=> x _ a b ab; rewrite lee_fin; exact/lefP/g_nd. + - by move=> x _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. Lemma fubini_tonelli1 : \int[m1 \x m2]_z f z = \int[m1]_x F x. Proof. -have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). +pose g := nnsfun_approx measurableT mf. have F_F x : F x = limn (F_ g ^~ x). rewrite [RHS](_ : _ = limn (fun n => \int[m2]_y (EFin \o g n) (x, y)))//. rewrite -monotone_convergence//; last 3 first. - by move=> n; exact/measurable_EFinP/measurableT_comp. - by move=> n /= y _; rewrite lee_fin; exact: fun_ge0. - - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: g_f. + - by move=> y /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. rewrite [RHS](_ : _ = limn (fun n => \int[m1 \x m2]_z (EFin \o g n) z)). rewrite -monotone_convergence //; last 3 first. - by move=> n; exact/measurable_EFinP. - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0. - - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. - by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: g_f. + - by move=> y /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. rewrite [LHS](_ : _ = limn (fun n => \int[m1]_x (\int[m2]_y (EFin \o g n) (x, y)))). set r := fun _ => _; set l := fun _ => _; have -> // : l = r. @@ -5571,26 +5601,26 @@ rewrite -monotone_convergence //; first exact: eq_integral. + exact/measurable_EFinP/measurableT_comp. + by move=> *; rewrite lee_fin; exact: fun_ge0. + exact/measurable_EFinP/measurableT_comp. - + by move=> y _; rewrite lee_fin; move/g_nd : ab => /lefP; exact. + + by move=> y _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. Lemma fubini_tonelli2 : \int[m1 \x m2]_z f z = \int[m2]_y G y. Proof. -have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). +pose g := nnsfun_approx measurableT mf. have G_G y : G y = limn (G_ g ^~ y). rewrite /G /fubini_G. rewrite [RHS](_ : _ = limn (fun n => \int[m1]_x (EFin \o g n) (x, y)))//. rewrite -monotone_convergence//; last 3 first. - by move=> n; exact/measurable_EFinP/measurableT_comp. - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0. - - by move=> x /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. - by apply: eq_integral => x _; apply/esym/cvg_lim => //; exact: g_f. + - by move=> x /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => x _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. rewrite [RHS](_ : _ = limn (fun n => \int[m1 \x m2]_z (EFin \o g n) z)). rewrite -monotone_convergence //; last 3 first. - by move=> n; exact/measurable_EFinP. - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0. - - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. - by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: g_f. + - by move=> y /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. rewrite [LHS](_ : _ = limn (fun n => \int[m2]_y (\int[m1]_x (EFin \o g n) (x, y)))). set r := fun _ => _; set l := fun _ => _; have -> // : l = r. @@ -5604,7 +5634,7 @@ rewrite -monotone_convergence //; first exact: eq_integral. + exact/measurable_EFinP/measurableT_comp. + by move=> *; rewrite lee_fin fun_ge0. + exact/measurable_EFinP/measurableT_comp. - + by move=> x _; rewrite lee_fin; move/g_nd : ab => /lefP; exact. + + by move=> x _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. Lemma fubini_tonelli : diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 5fbc202ca..48afe4f58 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1113,7 +1113,7 @@ apply: (@measurable_fun_limn_sup _ h) => // t Dt. - by apply/bounded_fun_has_lbound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. Qed. -Lemma measurable_fun_indic D (U : set T) : measurable U -> +Lemma measurable_indic D (U : set T) : measurable U -> measurable_fun D (\1_U : _ -> R). Proof. move=> mU mD /= Y mY. @@ -1133,6 +1133,16 @@ have [Y0|Y0] := pselect (Y 0%R); have [Y1|Y1] := pselect (Y 1%R). by apply/seteqP; split => // r /= -[_]; rewrite indicE; case: (_ \in _). Qed. +Lemma measurable_indicP D : measurable D <-> measurable_fun setT (\1_D : _ -> R). +Proof. +split=> [|m1]; first exact: measurable_indic. +have -> : D = (\1_D : _ -> R) @^-1` `]0, +oo[. + apply/seteqP; split => t/=. + by rewrite indicE => /mem_set ->; rewrite in_itv/= ltr01. + by rewrite in_itv/= andbT indicE ltr0n; have [/set_mem|//] := boolP (t \in D). +by rewrite -[_ @^-1` _]setTI; exact: m1. +Qed. + End measurable_fun_realType. #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_sup`")] Notation measurable_fun_lim_sup := measurable_fun_limn_sup (only parsing). @@ -1447,7 +1457,7 @@ Notation EFin_measurable_fun := measurable_EFinP (only parsing). Lemma measurable_fun_dirac d {T : measurableType d} {R : realType} D (U : set T) : measurable U -> measurable_fun D (fun x => \d_x U : \bar R). -Proof. by move=> /measurable_fun_indic/measurable_EFinP. Qed. +Proof. by move=> /measurable_indic/measurable_EFinP. Qed. Lemma measurable_er_map d (T : measurableType d) (R : realType) (f : R -> R) : measurable_fun setT f -> measurable_fun [set: \bar R] (er_map f).