From ce415a68dfa384abae730e5e090b69a09b86afe2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 5 Nov 2024 11:35:42 +0900 Subject: [PATCH] expectation of product --- CHANGELOG_UNRELEASED.md | 56 ++++ reals/constructive_ereal.v | 25 ++ theories/charge.v | 14 +- theories/kernel.v | 49 ++-- theories/lebesgue_integral.v | 234 +++++++++-------- theories/lebesgue_measure.v | 20 +- theories/measure.v | 70 +++++ theories/numfun.v | 165 +++++++++++- theories/probability.v | 479 ++++++++++++++++++++++++++++++++++- theories/realfun.v | 2 +- 10 files changed, 968 insertions(+), 146 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 260152313..2ff5543c7 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -92,6 +92,46 @@ + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and `max_fun_continuous`. +- in `constructive_ereal.v`: + + notation `\prod_( i <- r | P ) F` for extended real numbers and its variants + +- in `numfun.v`: + + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` + + lemmas `funrpos_ge0`, `funrneg_ge0`, `funrposN`, `funrnegN`, `ge0_funrposE`, + `ge0_funrnegE`, `le0_funrposE`, `le0_funrnegE`, `ge0_funrposM`, `ge0_funrnegM`, + `le0_funrposM`, `le0_funrnegM`, `funr_normr`, `funrposneg`, `funrD_Dpos`, + `funrD_posD`, `funrpos_le`, `funrneg_le` + + lemmas `funerpos`, `funerneg` + +- in `measure.v`: + + lemma `preimage_class_comp` + + defintions `mapping_display`, `g_sigma_algebra_mappingType`, `g_sigma_algebra_mapping`, + notations `.-mapping`, `.-mapping.-measurable` + +- in `lebesgue_measure.v`: + + lemma `measurable_indicP` + + lemmas `measurable_funrpos`, `measurable_funrneg` + +- in `lebesgue_integral.v`: + + definition `approx_A` (was `Let A`) + + definition `approx_B` (was `Let B`) + + lemma `measurable_fun_sum` + + lemma `integrable_indic` + +- in `probability.v`: + + lemma `expectationM_ge0` + + definition `independent_events` + + definition `mutual_independence` + + definition `independent_RVs` + + definition `independent_RVs2` + + lemmas `g_sigma_algebra_mapping_comp`, `g_sigma_algebra_mapping_funrpos`, + `g_sigma_algebra_mapping_funrneg` + + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`, + `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`, + `independent_RVs2_funrpospos` + + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`, + ` expectation_prod` + ### Changed - in file `normedtype.v`, @@ -143,10 +183,19 @@ `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`, `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`. +- in `lebesgue_integrale.v` + + change implicits of `measurable_funP` + ### Changed ### Renamed +- in `lebesgue_measure.v`: + + `measurable_fun_indic` -> `measurable_indic` + +- in `probability.v`: + + `expectationM` -> `expectationMl` + ### Generalized - in `lebesgue_integral.v`: @@ -161,6 +210,9 @@ - in `topology_structure.v`: + lemma `closureC` +- in file `lebesgue_integral.v`: + + lemma `approximation` + ### Removed - in `lebesgue_integral.v`: @@ -175,6 +227,10 @@ + lemma `cst_nnfun_subproof` (turned into a `Let`) + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead) +- 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/reals/constructive_ereal.v b/reals/constructive_ereal.v index a2155ef0e..27875e3f1 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -551,6 +551,31 @@ Notation "\sum_ ( i 'in' A ) F" := Notation "\sum_ ( i 'in' A ) F" := (\big[+%E/0%E]_(i in A) F%E) : ereal_scope. +Notation "\prod_ ( i <- r | P ) F" := + (\big[*%E/1%:E]_(i <- r | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i <- r ) F" := + (\big[*%E/1%:E]_(i <- r) F%E) : ereal_scope. +Notation "\prod_ ( m <= i < n | P ) F" := + (\big[*%E/1%:E]_(m <= i < n | P%B) F%E) : ereal_scope. +Notation "\prod_ ( m <= i < n ) F" := + (\big[*%E/1%:E]_(m <= i < n) F%E) : ereal_scope. +Notation "\prod_ ( i | P ) F" := + (\big[*%E/1%:E]_(i | P%B) F%E) : ereal_scope. +Notation "\prod_ i F" := + (\big[*%E/1%:E]_i F%E) : ereal_scope. +Notation "\prod_ ( i : t | P ) F" := + (\big[*%E/1%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope. +Notation "\prod_ ( i : t ) F" := + (\big[*%E/1%:E]_(i : t) F%E) (only parsing) : ereal_scope. +Notation "\prod_ ( i < n | P ) F" := + (\big[*%E/1%:E]_(i < n | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i < n ) F" := + (\big[*%E/1%:E]_(i < n) F%E) : ereal_scope. +Notation "\prod_ ( i 'in' A | P ) F" := + (\big[*%E/1%:E]_(i in A | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i 'in' A ) F" := + (\big[*%E/1%:E]_(i in A) F%E) : ereal_scope. + Section ERealOrderTheory. Context {R : numDomainType}. Implicit Types x y z : \bar R. diff --git a/theories/charge.v b/theories/charge.v index 498cc2228..b1452b7db 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 b043af47c..19352c4bb 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. *) @@ -222,8 +226,8 @@ HB.instance Definition _ x := isMeasurableFun.Build d _ aT rT (cst x) End mfun. -Section mfun_realType. -Context {d} {aT : sigmaRingType d} {rT : realType}. +Section mfun_sigmaRing_realType. +Context {rT : realType}. HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT (@normr rT rT) (@normr_measurable rT setT). @@ -231,7 +235,7 @@ HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT HB.instance Definition _ := isMeasurableFun.Build _ _ _ _ (@expR rT) (@measurable_expR rT). -End mfun_realType. +End mfun_sigmaRing_realType. Section mfun_measurableType. Context {d d'} {aT : measurableType d} {rT : measurableType d'}. @@ -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}. @@ -1042,7 +1038,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 ']'"). @@ -1095,9 +1091,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. @@ -1312,10 +1308,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. @@ -1617,6 +1616,7 @@ move=> m n mn; rewrite (nnsfun_approxE n) (nnsfun_approxE m). exact: nd_approx. Qed. +#[deprecated(since="mathcomp-analysis 1.7.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). @@ -1644,21 +1644,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. @@ -1686,29 +1686,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) -> @@ -1721,24 +1720,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. @@ -1760,16 +1759,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. @@ -2055,6 +2052,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). @@ -2396,13 +2409,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. @@ -2483,20 +2497,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 => //. @@ -2504,7 +2518,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. @@ -2653,19 +2667,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` _)). @@ -2699,16 +2713,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//. @@ -2812,8 +2825,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. @@ -2825,12 +2837,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. @@ -2838,8 +2850,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. @@ -3054,9 +3066,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 := @@ -3289,6 +3301,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). @@ -3305,7 +3335,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]. @@ -5523,49 +5553,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. @@ -5580,26 +5610,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. @@ -5613,7 +5643,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 e658b9a26..4b3b5b7b8 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1053,6 +1053,12 @@ by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; [exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf]. Qed. +Lemma measurable_funrpos D f : measurable_fun D f -> measurable_fun D f^\+. +Proof. by move=> mf; exact: measurable_maxr. Qed. + +Lemma measurable_funrneg D f : measurable_fun D f -> measurable_fun D f^\-. +Proof. by move=> mf; apply: measurable_maxr => //; exact: measurableT_comp. Qed. + Lemma measurable_minr D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g). Proof. @@ -1113,7 +1119,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 +1139,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 +1463,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). diff --git a/theories/measure.v b/theories/measure.v index 6cfd34f05..083028369 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -70,6 +70,11 @@ From HB Require Import structures. (* G.-sigma.-measurable A == A is measurable for the sigma-algebra <> *) (* g_sigma_algebraType G == the measurableType corresponding to <> *) (* This is an HB alias. *) +(* g_sigma_algebra_mapping f == sigma-algebra generated by the mapping f *) +(* g_sigma_algebra_mappingType f == the measurableType corresponding to *) +(* g_sigma_algebra_mapping f *) +(* This is an HB alias. *) +(* f.-mapping.-measurable A == A is measurable for g_sigma_algebra_mapping f *) (* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets *) (* ``` *) (* *) @@ -296,6 +301,9 @@ Reserved Notation "'\d_' a" (at level 8, a at level 2, format "'\d_' a"). Reserved Notation "G .-sigma" (at level 1, format "G .-sigma"). Reserved Notation "G .-sigma.-measurable" (at level 2, format "G .-sigma.-measurable"). +Reserved Notation "f .-mapping" (at level 1, format "f .-mapping"). +Reserved Notation "f .-mapping.-measurable" + (at level 2, format "f .-mapping.-measurable"). Reserved Notation "d .-ring" (at level 1, format "d .-ring"). Reserved Notation "d .-ring.-measurable" (at level 2, format "d .-ring.-measurable"). @@ -1735,6 +1743,16 @@ Definition preimage_class (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set rT)) : set (set aT) := [set D `&` f @^-1` B | B in G]. +Lemma preimage_class_comp (aT : Type) + d (rT : measurableType d) d' (T : sigmaRingType d') + (g : rT -> T) (f : aT -> rT) (D : set aT) : + measurable_fun setT g -> + preimage_class D (g \o f) measurable `<=` preimage_class D f measurable. +Proof. +move=> mg A; rewrite /preimage_class/= => -[B GB]; exists (g @^-1` B) => //. +by rewrite -[X in measurable X]setTI; exact: mg. +Qed. + (* f is measurable on the sigma-algebra generated by itself *) Lemma preimage_class_measurable_fun d (aT : pointedType) (rT : measurableType d) (D : set aT) (f : aT -> rT) : @@ -1819,6 +1837,58 @@ Qed. End measurability. +Definition mapping_display {T T'} : (T -> T') -> measure_display. +Proof. exact. Qed. + +Definition g_sigma_algebra_mappingType d' (T : pointedType) + (T' : measurableType d') (f : T -> T') : Type := T. + +Definition g_sigma_algebra_mapping d' (T : pointedType) + (T' : measurableType d') (f : T -> T') := + preimage_class setT f (@measurable _ T'). + +Section mapping_generated_sigma_algebra. +Context {d'} (T : pointedType) (T' : measurableType d'). +Variable f : T -> T'. + +Let mapping_set0 : g_sigma_algebra_mapping f set0. +Proof. +rewrite /g_sigma_algebra_mapping /preimage_class/=. +by exists set0 => //; rewrite preimage_set0 setI0. +Qed. + +Let mapping_setC A : + g_sigma_algebra_mapping f A -> g_sigma_algebra_mapping f (~` A). +Proof. +rewrite /g_sigma_algebra_mapping /preimage_class/= => -[B mB] <-{A}. +by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC]. +Qed. + +Let mapping_bigcup (F : (set T)^nat) : + (forall i, g_sigma_algebra_mapping f (F i)) -> + g_sigma_algebra_mapping f (\bigcup_i (F i)). +Proof. +move=> mF; rewrite /g_sigma_algebra_mapping /preimage_class/=. +pose g := fun i => sval (cid2 (mF i)). +pose mg := fun i => svalP (cid2 (mF i)). +exists (\bigcup_i g i). + by apply: bigcup_measurable => k; case: (mg k). +rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _. +by case: (mg k) => _; rewrite setTI. +Qed. + +HB.instance Definition _ := Pointed.on (g_sigma_algebra_mappingType f). + +HB.instance Definition _ := @isMeasurable.Build (mapping_display f) + (g_sigma_algebra_mappingType f) (g_sigma_algebra_mapping f) + mapping_set0 mapping_setC mapping_bigcup. + +End mapping_generated_sigma_algebra. + +Notation "f .-mapping" := (mapping_display f) : measure_display_scope. +Notation "f .-mapping.-measurable" := + (measurable : set (set (g_sigma_algebra_mappingType f))) : classical_set_scope. + Local Open Scope ereal_scope. Definition subset_sigma_subadditive {T} {R : numFieldType} diff --git a/theories/numfun.v b/theories/numfun.v index f3361cce0..d38b7216e 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -14,12 +14,15 @@ From mathcomp Require Import function_spaces. (* ``` *) (* {nnfun T >-> R} == type of non-negative functions *) (* f ^\+ == the function formed by the non-negative outputs *) -(* of f (from a type to the type of extended real *) -(* numbers) and 0 otherwise *) -(* rendered as f ⁺ with company-coq (U+207A) *) +(* of f and 0 otherwise *) +(* The codomain of f is the real numbers in scope *) +(* ring_scope and the extended real numbers in scope *) +(* ereal_scope. *) +(* It is rendered as f ⁺ with company-coq (U+207A). *) (* f ^\- == the function formed by the non-positive outputs *) (* of f and 0 o.w. *) -(* rendered as f ⁻ with company-coq (U+207B) *) +(* Similar to ^\+. *) +(* It is rendered as f ⁻ with company-coq (U+207B). *) (* \1_ A == indicator function 1_A *) (* ``` *) (* *) @@ -127,6 +130,149 @@ Proof. by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?mule0. Qed. End erestrict_lemmas. +Section funrposneg. +Local Open Scope ring_scope. + +Definition funrpos T (R : realDomainType) (f : T -> R) := + fun x => maxr (f x) 0. +Definition funrneg T (R : realDomainType) (f : T -> R) := + fun x => maxr (- f x) 0. + +End funrposneg. + +Notation "f ^\+" := (funrpos f) : ring_scope. +Notation "f ^\-" := (funrneg f) : ring_scope. + +Section funrposneg_lemmas. +Local Open Scope ring_scope. +Variables (T : Type) (R : realDomainType) (D : set T). +Implicit Types (f g : T -> R) (r : R). + +Lemma funrpos_ge0 f x : 0 <= f^\+ x. +Proof. by rewrite /funrpos /= le_max lexx orbT. Qed. + +Lemma funrneg_ge0 f x : 0 <= f^\- x. +Proof. by rewrite /funrneg le_max lexx orbT. Qed. + +Lemma funrposN f : (\- f)^\+ = f^\-. Proof. exact/funext. Qed. + +Lemma funrnegN f : (\- f)^\- = f^\+. +Proof. by apply/funext => x; rewrite /funrneg opprK. Qed. + +(* TODO: the following lemmas require a pointed type and realDomainType does +not seem to be at this point + +Lemma funrpos_restrict f : (f \_ D)^\+ = (f^\+) \_ D. +Proof. +by apply/funext => x; rewrite /patch/_^\+; case: ifP; rewrite //= maxxx. +Qed. + +Lemma funrneg_restrict f : (f \_ D)^\- = (f^\-) \_ D. +Proof. +by apply/funext => x; rewrite /patch/_^\-; case: ifP; rewrite //= oppr0 maxxx. +Qed.*) + +Lemma ge0_funrposE f : (forall x, D x -> 0 <= f x) -> {in D, f^\+ =1 f}. +Proof. by move=> f0 x; rewrite inE => Dx; apply/max_idPl/f0. Qed. + +Lemma ge0_funrnegE f : (forall x, D x -> 0 <= f x) -> {in D, f^\- =1 cst 0}. +Proof. +by move=> f0 x; rewrite inE => Dx; apply/max_idPr; rewrite lerNl oppr0 f0. +Qed. + +Lemma le0_funrposE f : (forall x, D x -> f x <= 0) -> {in D, f^\+ =1 cst 0}. +Proof. by move=> f0 x; rewrite inE => Dx; exact/max_idPr/f0. Qed. + +Lemma le0_funrnegE f : (forall x, D x -> f x <= 0) -> {in D, f^\- =1 \- f}. +Proof. +by move=> f0 x; rewrite inE => Dx; apply/max_idPl; rewrite lerNr oppr0 f0. +Qed. + +Lemma ge0_funrposM r f : (0 <= r)%R -> + (fun x => r * f x)^\+ = (fun x => r * (f^\+ x)). +Proof. by move=> ?; rewrite funeqE => x; rewrite /funrpos maxr_pMr// mulr0. Qed. + +Lemma ge0_funrnegM r f : (0 <= r)%R -> + (fun x => r * f x)^\- = (fun x => r * (f^\- x)). +Proof. +by move=> r0; rewrite funeqE => x; rewrite /funrneg -mulrN maxr_pMr// mulr0. +Qed. + +Lemma le0_funrposM r f : (r <= 0)%R -> + (fun x => r * f x)^\+ = (fun x => - r * (f^\- x)). +Proof. +move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr. +by rewrite funrposN ge0_funrnegM ?oppr_ge0. +Qed. + +Lemma le0_funrnegM r f : (r <= 0)%R -> + (fun x => r * f x)^\- = (fun x => - r * (f^\+ x)). +Proof. +move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr. +by rewrite funrnegN ge0_funrposM ?oppr_ge0. +Qed. + +Lemma funr_normr f : normr \o f = f^\+ \+ f^\-. +Proof. +rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0. +- rewrite ler0_norm// /funrpos /funrneg. + move/max_idPr : (fx0) => ->; rewrite add0r. + by move: fx0; rewrite -{1}oppr0 lerNr => /max_idPl ->. +- rewrite ger0_norm// /funrpos /funrneg; move/max_idPl : (fx0) => ->. + by move: fx0; rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0. +Qed. + +Lemma funrposneg f : f = (fun x => f^\+ x - f^\- x). +Proof. +rewrite funeqE => x; rewrite /funrpos /funrneg; have [|/ltW] := leP (f x) 0. + by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r. +by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0. +Qed. + +Lemma funrD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-. +Proof. +apply/funext => x; rewrite /funrpos /funrneg/=; have [|/ltW] := lerP 0 (f x + g x). +- by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0. +- by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r. +Qed. + +Lemma funrD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-). +Proof. +apply/funext => x; rewrite /funrpos /funrneg/=. +have [|fx0] := lerP 0 (f x); last rewrite add0r. +- rewrite -{1}oppr0 lerNl => /max_idPr ->; have [|/ltW] := lerP 0 (g x). + by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 subr0. + by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite addr0 sub0r opprK. +- move/ltW : (fx0); rewrite -{1}oppr0 lerNr => /max_idPl ->. + have [|]/= := lerP 0 (g x); last rewrite add0r. + by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 opprK addrC. + by rewrite -oppr0 ltrNr -{1}oppr0 => /ltW/max_idPl ->; rewrite opprD !opprK. +Qed. + +Lemma funrpos_le f g : + {in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}. +Proof. +move=> fg x Dx; rewrite /funrpos /maxr; case: ifPn => fx; case: ifPn => gx //. +- by rewrite leNgt. +- by move: fx; rewrite -leNgt => /(lt_le_trans gx); rewrite ltNge fg. +- exact: fg. +Qed. + +Lemma funrneg_le f g : + {in D, forall x, f x <= g x} -> {in D, forall x, g^\- x <= f^\- x}. +Proof. +move=> fg x Dx; rewrite /funrneg /maxr; case: ifPn => gx; case: ifPn => fx //. +- by rewrite leNgt. +- by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite ltrN2 ltNge fg. +- by rewrite lerN2; exact: fg. +Qed. + +End funrposneg_lemmas. +#[global] +Hint Extern 0 (is_true (0%R <= _ ^\+ _)%R) => solve [apply: funrpos_ge0] : core. +#[global] +Hint Extern 0 (is_true (0%R <= _ ^\- _)%R) => solve [apply: funrneg_ge0] : core. + Section funposneg. Local Open Scope ereal_scope. @@ -276,6 +422,17 @@ Hint Extern 0 (is_true (0%R <= _ ^\+ _)%E) => solve [apply: funepos_ge0] : core. #[global] Hint Extern 0 (is_true (0%R <= _ ^\- _)%E) => solve [apply: funeneg_ge0] : core. +Section funrpos_funepos_lemmas. +Context {T : Type} {R : realDomainType}. + +Lemma funerpos (f : T -> R) : (EFin \o f)^\+%E = (EFin \o f^\+). +Proof. by apply/funext => x; rewrite /funepos /funrpos/= EFin_max. Qed. + +Lemma funerneg (f : T -> R) : (EFin \o f)^\-%E = (EFin \o f^\-). +Proof. by apply/funext => x; rewrite /funeneg /funrneg/= EFin_max. Qed. + +End funrpos_funepos_lemmas. + Definition indic {T} {R : ringType} (A : set T) (x : T) : R := (x \in A)%:R. Reserved Notation "'\1_' A" (at level 8, A at level 2, format "'\1_' A") . Notation "'\1_' A" := (indic A) : ring_scope. diff --git a/theories/probability.v b/theories/probability.v index c57cac324..25b0a7b73 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -34,6 +34,10 @@ From mathcomp Require Import lebesgue_integral kernel. (* dRV_enum X == bijection between the domain and the range of X *) (* pmf X r := fine (P (X @^-1` [set r])) *) (* enum_prob X k == probability of the kth value in the range of X *) +(* independent_events I F == the events F indexed by I are independent *) +(* mutual_independence I F == the classes F indexed by I are independent *) +(* independent_RVs I X == the random variables X indexed by I are independent *) +(* independent_RVs2 X Y == the random variables X and Y are independent *) (* ``` *) (* *) (* ``` *) @@ -141,6 +145,9 @@ Section expectation_lemmas. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). +Lemma expectation_def (X : {RV P >-> R}) : 'E_P[X] = (\int[P]_w (X w)%:E)%E. +Proof. by rewrite unlock. Qed. + Lemma expectation_fin_num (X : {RV P >-> R}) : P.-integrable setT (EFin \o X) -> 'E_P[X] \is a fin_num. Proof. by move=> ?; rewrite unlock integral_fune_fin_num. Qed. @@ -158,7 +165,7 @@ move: iX => /integrableP[? Xoo]; rewrite (le_lt_trans _ Xoo)// unlock. exact: le_trans (le_abse_integral _ _ _). Qed. -Lemma expectationM (X : {RV P >-> R}) (iX : P.-integrable [set: T] (EFin \o X)) +Lemma expectationMl (X : {RV P >-> R}) (iX : P.-integrable [set: T] (EFin \o X)) (k : R) : 'E_P[k \o* X] = k%:E * 'E_P [X]. Proof. by rewrite unlock muleC -integralZr. Qed. @@ -208,6 +215,8 @@ by apply/funext => t/=; rewrite big_map sumEFin mfun_sum. Qed. End expectation_lemmas. +#[deprecated(since="mathcomp-analysis 1.7.0", note="use `expectationMl` instead")] +Notation expectationM := expectationMl (only parsing). HB.lock Definition covariance {d} {T : measurableType d} {R : realType} (P : probability T R) (X Y : T -> R) := @@ -238,7 +247,7 @@ rewrite expectationD/=; last 2 first. - by rewrite compreBr// integrableB// compre_scale ?integrableZl. - by rewrite compre_scale// integrableZl// finite_measure_integrable_cst. rewrite 2?expectationB//= ?compre_scale// ?integrableZl//. -rewrite 3?expectationM//= ?finite_measure_integrable_cst//. +rewrite 3?expectationMl//= ?finite_measure_integrable_cst//. by rewrite expectation_cst mule1 fineM// EFinM !fineK// muleC subeK ?fin_numM. Qed. @@ -278,7 +287,7 @@ have aXY : (a \o* X * Y = a \o* (X * Y))%R. rewrite [LHS]covarianceE => [||//|] /=; last 2 first. - by rewrite compre_scale ?integrableZl. - by rewrite aXY compre_scale ?integrableZl. -rewrite covarianceE// aXY !expectationM//. +rewrite covarianceE// aXY !expectationMl//. by rewrite -muleA -muleBr// fin_num_adde_defr// expectation_fin_num. Qed. @@ -525,6 +534,24 @@ Qed. End variance. Notation "'V_ P [ X ]" := (variance P X). +(* TODO: move earlier *) +Section mfun_measurable_realType. +Context {d} {aT : measurableType d} {rT : realType}. + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\+ + (measurable_funrpos (@measurable_funP _ _ _ _ f)). + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\- + (measurable_funrneg (@measurable_funP _ _ _ _ f)). + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ (@normr _ _ \o f) + (measurableT_comp (@normr_measurable _ _) (@measurable_funP _ _ _ _ f)). + +End mfun_measurable_realType. + Section markov_chebyshev_cantelli. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). @@ -554,7 +581,7 @@ Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R -> Proof. move=> t0. rewrite /mmt_gen_fun; have -> : expR \o r \o* X = - (normr \o normr) \o [the {mfun T >-> R} of expR \o r \o* X]. + (normr \o normr) \o [the {mfun _ >-> _} of expR \o r \o* X]. by apply: funext => t /=; rewrite normr_id ger0_norm ?expR_ge0. rewrite expRN lee_pdivlMr ?expR_gt0//. rewrite (le_trans _ (markov _ (expR_gt0 (r * a)) _ _ _))//; last first. @@ -841,6 +868,438 @@ Qed. End discrete_distribution. +Section independent_events. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Definition independent_events (I0 : choiceType) (I : set I0) (A : I0 -> set T) := + forall J : {fset I0}, [set` J] `<=` I -> + P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i). + +End independent_events. + +Section mutual_independence. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Definition mutual_independence (I0 : choiceType) (I : set I0) + (F : I0 -> set (set T)) := + (forall i : I0, I i -> F i `<=` @measurable _ T) /\ + forall J : {fset I0}, + [set` J] `<=` I -> + forall E : I0 -> set T, + (forall i : I0, i \in J -> E i \in F i) -> + P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j). + +End mutual_independence. + +Section independent_RVs. +Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). +Variable P : probability T R. + +Definition independent_RVs (I0 : choiceType) (I : set I0) + (X : I0 -> {mfun T >-> T'}) : Prop := + mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). + +Definition independent_RVs2 (X Y : {mfun T >-> T'}) := + independent_RVs [set 0%N; 1%N] + [eta (fun=> cst point) with 0%N |-> X, 1%N |-> Y]. + +End independent_RVs. + +Section g_sigma_algebra_mapping_lemmas. +Context d {T : measurableType d} {R : realType}. + +Lemma g_sigma_algebra_mapping_comp (X : {mfun T >-> R}) (f : R -> R) : + measurable_fun setT f -> + g_sigma_algebra_mapping (f \o X)%R `<=` g_sigma_algebra_mapping X. +Proof. exact: preimage_class_comp. Qed. + +Lemma g_sigma_algebra_mapping_funrpos (X : {mfun T >-> R}) : + g_sigma_algebra_mapping X^\+%R `<=` d.-measurable. +Proof. +by move=> A/= -[B mB] <-; have := measurable_funrpos (measurable_funP X); exact. +Qed. + +Lemma g_sigma_algebra_mapping_funrneg (X : {mfun T >-> R}) : + g_sigma_algebra_mapping X^\-%R `<=` d.-measurable. +Proof. +by move=> A/= -[B mB] <-; have := measurable_funrneg (measurable_funP X); exact. +Qed. + +End g_sigma_algebra_mapping_lemmas. +Arguments g_sigma_algebra_mapping_comp {d T R X} f. + +Section independent_RVs_lemmas. +Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). +Variable P : probability T R. +Local Open Scope ring_scope. + +Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y). +Proof. +move=> indeXY; split => [i [|]->{i}/= Z/=|J J01 E JE]. +- by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; + exact/measurableT_comp. +- by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; + exact/measurableT_comp. +- apply indeXY => //= i iJ; have := JE _ iJ. + have : i \in [set 0%N; 1%N] by rewrite inE; apply: J01. + rewrite inE/= => -[|] /eqP ->/=; rewrite !inE. + + exact: g_sigma_algebra_mapping_comp. + + by case: ifPn => [/eqP ->|i0]; exact: g_sigma_algebra_mapping_comp. +Qed. + +Lemma independent_RVs2_funrposneg (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-. +Proof. +move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. +Qed. + +Lemma independent_RVs2_funrnegpos (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+. +Proof. +move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrpos. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. +Qed. + +Lemma independent_RVs2_funrnegneg (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-. +Proof. +move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. +Qed. + +Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. +Proof. +move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrpos. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. +Qed. + +End independent_RVs_lemmas. + +Section product_expectation. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. +Local Open Scope ereal_scope. + +Import HBNNSimple. + +Let expectationM_nnsfun (f g : {nnsfun T >-> R}) : + (forall y y', y \in range f -> y' \in range g -> + P (f @^-1` [set y] `&` g @^-1` [set y']) = + P (f @^-1` [set y]) * P (g @^-1` [set y'])) -> + 'E_P [f \* g] = 'E_P [f] * 'E_P [g]. +Proof. +move=> fg; transitivity + ('E_P [(fun x => (\sum_(y \in range f) y * \1_(f @^-1` [set y]) x)%R) + \* (fun x => (\sum_(y \in range g) y * \1_(g @^-1` [set y]) x)%R)]). + by congr ('E_P [_]); apply/funext => t/=; rewrite (fimfunE f) (fimfunE g). +transitivity ('E_P [(fun x => (\sum_(y \in range f) \sum_(y' \in range g) y * y' + * \1_(f @^-1` [set y] `&` g @^-1` [set y']) x)%R)]). + congr ('E_P [_]); apply/funext => t/=. + rewrite mulrC; rewrite fsbig_distrr//=. (* TODO: lemma fsbig_distrl *) + apply: eq_fsbigr => y yf; rewrite mulrC; rewrite fsbig_distrr//=. + by apply: eq_fsbigr => y' y'g; rewrite indicI mulrCA !mulrA (mulrC y'). +rewrite unlock. +under eq_integral do rewrite -fsumEFin//. +transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + ((y * y')%:E * \int[P]_w (\1_(f @^-1` [set y] `&` g @^-1` [set y']) w)%:E))). + rewrite ge0_integral_fsum//=; last 2 first. + - move=> r; under eq_fun do rewrite -fsumEFin//. + apply: emeasurable_fun_fsum => // s. + apply/measurable_EFinP/measurable_funM => //. + exact/measurable_indic/measurableI. + - move=> r t _; rewrite lee_fin sumr_ge0 // => s _; rewrite -lee_fin. + by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. + apply: eq_fsbigr => y yf. + under eq_integral do rewrite -fsumEFin//. + rewrite ge0_integral_fsum//=; last 2 first. + - move=> r; apply/measurable_EFinP; apply: measurable_funM => //. + exact/measurable_indic/measurableI. + - move=> r t _. + by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. + apply: eq_fsbigr => y' y'g. + under eq_integral do rewrite EFinM. + by rewrite integralZl//; exact/integrable_indic/measurableI. +transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + ((y * y')%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E * + \int[P]_w (\1_(g @^-1` [set y']) w)%:E)))). + apply: eq_fsbigr => y fy; apply: eq_fsbigr => y' gy'; congr *%E. + transitivity ('E_P[\1_(f @^-1` [set y] `&` g @^-1` [set y'])]). + by rewrite unlock. + transitivity ('E_P[\1_(f @^-1` [set y])] * 'E_P[\1_(g @^-1` [set y'])]); + last by rewrite unlock. + rewrite expectation_indic//; last exact: measurableI. + by rewrite !expectation_indic// fg. +transitivity ( + (\sum_(y \in range f) (y%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E))) * + (\sum_(y' \in range g) (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E))). + transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E)%E)%R * + (y%:E * \int[P]_w (\1_(f @^-1` [set y]) w)%:E)%E%R); last first. + rewrite !fsbig_finite//= ge0_sume_distrl//; last first. + move=> r _; rewrite -integralZl//; last exact: integrable_indic. + by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. + by apply: eq_bigr => r _; rewrite muleC. + apply: eq_fsbigr => y fy. + rewrite !fsbig_finite//= ge0_sume_distrl//; last first. + move=> r _; rewrite -integralZl//; last exact: integrable_indic. + by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. + apply: eq_bigr => r _; rewrite (mulrC y) EFinM. + by rewrite [X in _ * X]muleC muleACA. +suff: forall h : {nnsfun T >-> R}, + (\sum_(y \in range h) (y%:E * \int[P]_w (\1_(h @^-1` [set y]) w)%:E)%E)%R + = \int[P]_w (h w)%:E. + by move=> suf; congr *%E; rewrite suf. +move=> h. +apply/esym. +under eq_integral do rewrite (fimfunE h). +under eq_integral do rewrite -fsumEFin//. +rewrite ge0_integral_fsum//; last 2 first. +- by move=> r; exact/measurable_EFinP/measurable_funM. +- by move=> r t _; rewrite lee_fin -lee_fin nnfun_muleindic_ge0. +by apply: eq_fsbigr => y fy; rewrite -integralZl//; exact/integrable_indic. +Qed. + +Lemma expectationM_ge0 (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + 'E_P[X] *? 'E_P[Y] -> + (forall t, 0 <= X t)%R -> (forall t, 0 <= Y t)%R -> + 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. +Proof. +move=> indeXY defXY X0 Y0. +have mX : measurable_fun setT (EFin \o X) by exact/measurable_EFinP. +have mY : measurable_fun setT (EFin \o Y) by exact/measurable_EFinP. +pose X_ := nnsfun_approx measurableT mX. +pose Y_ := nnsfun_approx measurableT mY. +have EXY : 'E_P[X_ n \* Y_ n] @[n --> \oo] --> 'E_P [X * Y]. + rewrite unlock; have -> : \int[P]_w ((X * Y) w)%:E = + \int[P]_x limn (fun n => (EFin \o (X_ n \* Y_ n)%R) x). + apply: eq_integral => t _; apply/esym/cvg_lim => //=. + rewrite fctE EFinM; under eq_fun do rewrite EFinM. + by apply: cvgeM; [rewrite mule_def_fin//| + apply: cvg_nnsfun_approx => //= x _; rewrite lee_fin..]. + apply: cvg_monotone_convergence => //. + - by move=> n; apply/measurable_EFinP; exact: measurable_funM. + - by move=> n t _; rewrite lee_fin. + - move=> t _ m n mn. + by rewrite lee_fin/= ler_pM//; exact/lefP/nd_nnsfun_approx. +have EX : 'E_P[X_ n] @[n --> \oo] --> 'E_P [X]. + rewrite unlock. + have -> : \int[P]_w (X w)%:E = \int[P]_x limn (fun n => (EFin \o X_ n) x). + by apply: eq_integral => t _; apply/esym/cvg_lim => //=; + apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n t _; rewrite lee_fin. + - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. +have EY : 'E_P[Y_ n] @[n --> \oo] --> 'E_P [Y]. + rewrite unlock. + have -> : \int[P]_w (Y w)%:E = \int[P]_x limn (fun n => (EFin \o Y_ n) x). + by apply: eq_integral => t _; apply/esym/cvg_lim => //=; + apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n t _; rewrite lee_fin. + - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. +have {EX EY}EXY' : 'E_P[X_ n] * 'E_P[Y_ n] @[n --> \oo] --> 'E_P[X] * 'E_P[Y]. + apply: cvgeM => //. +suff : forall n, 'E_P[X_ n \* Y_ n] = 'E_P[X_ n] * 'E_P[Y_ n]. + by move=> suf; apply: (cvg_unique _ EXY) => //=; under eq_fun do rewrite suf. +move=> n; apply: expectationM_nnsfun => x y xX_ yY_. +suff : P (\big[setI/setT]_(j <- [fset 0%N; 1%N]%fset) + [eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], + 1%N |-> Y_ n @^-1` [set y]] j) = + \prod_(j <- [fset 0%N; 1%N]%fset) + P ([eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], + 1%N |-> Y_ n @^-1` [set y]] j). + by rewrite !big_fsetU1/= ?inE//= !big_seq_fset1/=. +move: indeXY => [/= _]; apply => // i. + by rewrite /= !inE => /orP[|]/eqP ->; auto. +pose AX := approx_A setT (EFin \o X). +pose AY := approx_A setT (EFin \o Y). +pose BX := approx_B setT (EFin \o X). +pose BY := approx_B setT (EFin \o Y). +have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> + g_sigma_algebra_mapping Z (approx_A setT (EFin \o Z) m k). + move=> mk; rewrite /g_sigma_algebra_mapping /approx_A mk setTI. + rewrite /preimage_class/=; exists [set` dyadic_itv R m k] => //. + rewrite setTI/=; apply/seteqP; split => z/=. + by rewrite inE/= => Zz; exists (Z z). + by rewrite inE/= => -[r rmk] [<-]. +have mB (Z : {RV P >-> R}) k : + g_sigma_algebra_mapping Z (approx_B setT (EFin \o Z) k). + rewrite /g_sigma_algebra_mapping /approx_B setTI /preimage_class/=. + by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itv_c_infty. +have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> + measurable_fun setT + (\1_(approx_A setT (EFin \o Z) n k) : g_sigma_algebra_mappingType Z -> R). + move=> k kn. + exact/(@measurable_indicP _ (g_sigma_algebra_mappingType Z))/mA. +rewrite !inE => /orP[|]/eqP->{i} //=. + have : @measurable_fun _ _ (g_sigma_algebra_mappingType X) _ setT (X_ n). + rewrite nnsfun_approxE//. + apply: measurable_funD => //=. + apply: measurable_fun_sum => //= k'; apply: measurable_funM => //. + by apply: measurable_indic; exact: mA. + apply: measurable_funM => //. + by apply: measurable_indic; exact: mB. + rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). + by rewrite setTI. +have : @measurable_fun _ _ (g_sigma_algebra_mappingType Y) _ setT (Y_ n). + rewrite nnsfun_approxE//. + apply: measurable_funD => //=. + apply: measurable_fun_sum => //= k'; apply: measurable_funM => //. + by apply: measurable_indic; exact: mA. + apply: measurable_funM => //. + by apply: measurable_indic; exact: mB. +move=> /(_ measurableT [set y] (measurable_set1 y)). +by rewrite setTI. +Qed. + +Lemma integrable_expectationM (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + `|'E_P [X * Y]| < +oo. +Proof. +move=> indeXY iX iY. +apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]). + rewrite unlock/=. + rewrite (le_trans (le_abse_integral _ _ _))//. + apply/measurable_EFinP/measurable_funM. + by have /measurable_EFinP := measurable_int _ iX. + by have /measurable_EFinP := measurable_int _ iY. + apply: ge0_le_integral => //=. + - by apply/measurable_EFinP; exact/measurableT_comp. + - by move=> x _; rewrite lee_fin/= mulr_ge0/=. + - by apply/measurable_EFinP; apply/measurable_funM; exact/measurableT_comp. + - by move=> t _; rewrite lee_fin/= normrM. +rewrite expectationM_ge0//=. +- rewrite lte_mul_pinfty//. + + by rewrite expectation_ge0/=. + + rewrite expectation_fin_num//= compA//. + exact: (integrable_abse iX). + + by move/integrableP : iY => [_ iY]; rewrite unlock. +- exact: independent_RVs2_comp. +- apply: mule_def_fin; rewrite unlock integral_fune_fin_num//. + + exact: (integrable_abse iX). + + exact: (integrable_abse iY). +Qed. + +Lemma independent_integrableM (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + P.-integrable setT (EFin \o (X \* Y)%R). +Proof. +move=> indeXY iX iY. +apply/integrableP; split; first exact/measurable_EFinP/measurable_funM. +have := integrable_expectationM indeXY iX iY. +rewrite unlock => /abse_integralP; apply => //. +exact/measurable_EFinP/measurable_funM. +Qed. + +(* TODO: rename to expectationM when deprecation is removed *) +Lemma expectation_prod (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. +Proof. +move=> XY iX iY. +transitivity ('E_P[(X^\+ - X^\-) * (Y^\+ - Y^\-)]). + congr ('E_P[_]). + apply/funext => /=t. + by rewrite [in LHS](funrposneg X)/= [in LHS](funrposneg Y). +have ? : P.-integrable [set: T] (EFin \o X^\-%R). + by rewrite -funerneg; exact/integrable_funeneg. +have ? : P.-integrable [set: T] (EFin \o X^\+%R). + by rewrite -funerpos; exact/integrable_funepos. +have ? : P.-integrable [set: T] (EFin \o Y^\+%R). + by rewrite -funerpos; exact/integrable_funepos. +have ? : P.-integrable [set: T] (EFin \o Y^\-%R). + by rewrite -funerneg; exact/integrable_funeneg. +have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\+)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrpospos. +have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\+)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegpos. +have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\-)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrposneg. +have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\-)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegneg. +transitivity ('E_P[X^\+ * Y^\+] - 'E_P[X^\- * Y^\+] + - 'E_P[X^\+ * Y^\-] + 'E_P[X^\- * Y^\-]). + rewrite mulrDr !mulrDl -expectationB//= -expectationB//=; last first. + rewrite (_ : _ \o _ = EFin \o (X^\+ \* Y^\+)%R \- + (EFin \o (X^\- \* Y^\+)%R))//. + exact: integrableB. + rewrite -expectationD//=; last first. + rewrite (_ : _ \o _ = (EFin \o (X^\+ \* Y^\+)%R) + \- (EFin \o (X^\- \* Y^\+)%R) \- (EFin \o (X^\+ \* Y^\-)%R))//. + by apply: integrableB => //; exact: integrableB. + congr ('E_P[_]); apply/funext => t/=. + by rewrite !fctE !(mulNr,mulrN,opprK,addrA)/=. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrpospos. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrnegpos. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrposneg. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrnegneg. + by rewrite mule_def_fin// expectation_fin_num//=. +transitivity ('E_P[X^\+ - X^\-] * 'E_P[Y^\+ - Y^\-]). + rewrite -addeA -addeACA -muleBr; last 2 first. + by rewrite expectation_fin_num. + by rewrite fin_num_adde_defr// expectation_fin_num. + rewrite -oppeB; last first. + by rewrite fin_num_adde_defr// fin_numM// expectation_fin_num. + rewrite -muleBr; last 2 first. + by rewrite expectation_fin_num. + by rewrite fin_num_adde_defr// expectation_fin_num. + rewrite -muleBl; last 2 first. + by rewrite fin_numB// !expectation_fin_num//. + by rewrite fin_num_adde_defr// expectation_fin_num. + by rewrite -expectationB//= -expectationB. +by congr *%E; congr ('E_P[_]); rewrite [RHS]funrposneg. +Qed. + +End product_expectation. + Section bernoulli_pmf. Context {R : realType} (p : R). Local Open Scope ring_scope. @@ -1323,21 +1782,21 @@ Lemma integral_uniform (f : _ -> \bar R) : (\int[uniform_prob ab]_x f x = (b - a)^-1%:E * \int[mu]_(x in `[a, b]) f x)%E. Proof. move=> mf f0. -have [f_ [ndf_ f_f]] := approximation measurableT mf (fun y _ => f0 y). +pose f_ := nnsfun_approx measurableT mf. transitivity (lim (\int[uniform_prob ab]_x (f_ n x)%:E @[n --> \oo])%E). rewrite -monotone_convergence//=. - apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //=. - exact: f_f. + exact/cvg_nnsfun_approx. - by move=> n; exact/measurable_EFinP/measurable_funTS. - by move=> n ? _; rewrite lee_fin. - - by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/ndf_. + - by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. rewrite [X in _ = (_ * X)%E](_ : _ = lim (\int[mu]_(x in `[a, b]) (f_ n x)%:E @[n --> \oo])%E); last first. rewrite -monotone_convergence//=. - - by apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //; exact: f_f. + - by apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. - by move=> n; exact/measurable_EFinP/measurable_funTS. - by move=> n ? _; rewrite lee_fin. - - by move=> ? _ ? ? /ndf_ /lefP; rewrite lee_fin. + - by move=> ? _ u v uv; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. rewrite -limeMl//. by apply: congr_lim; apply/funext => n /=; exact: integral_uniform_nnsfun. apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=. @@ -1345,7 +1804,7 @@ apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=. - exact/measurable_EFinP/measurable_funTS. - by move=> ? _; rewrite lee_fin. - exact/measurable_EFinP/measurable_funTS. -- by move=> ? _; rewrite lee_fin; move/ndf_ : xy => /lefP. +- by move=> ? _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. End uniform_probability. diff --git a/theories/realfun.v b/theories/realfun.v index ebf570f54..537658eee 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1,4 +1,5 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum archimedean. From mathcomp Require Import matrix interval zmodp vector fieldext falgebra. From mathcomp Require Import finmap. @@ -6,7 +7,6 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality ereal reals signed. From mathcomp Require Import topology prodnormedzmodule normedtype derive. From mathcomp Require Import sequences real_interval. -From HB Require Import structures. (**md**************************************************************************) (* # Real-valued functions over reals *)