From 822e624269ddbd44cb13267ff89da1c556283815 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 28 Dec 2023 00:36:47 +0900 Subject: [PATCH] rm one Local lemma --- CHANGELOG_UNRELEASED.md | 5 +- theories/charge.v | 115 ++++++++++++++++++---------------------- theories/sequences.v | 1 + 3 files changed, 58 insertions(+), 63 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c3af81cf6..9996fd5ab 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -65,7 +65,7 @@ + lemma `jordan_posE` + lemma `cjordan_negE` + lemma `jordan_negE` - + lemma `Radon_Nikodym_sigma_finite_fin_num` + + lemma `Radon_Nikodym_sigma_finite` + lemma `Radon_Nikodym_fin_num` + lemma `Radon_Nikodym_integral` + lemma `ae_eq_Radon_Nikodym_SigmaFinite` @@ -113,6 +113,9 @@ * lemma `integralM` * lemma `chain_rule` +- in `sequences.v`: + + change the implicit arguments of `trivIset_seqDU` + ### Renamed - in `exp.v`: diff --git a/theories/charge.v b/theories/charge.v index d4c278bbb..a46b48839 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1508,37 +1508,36 @@ Context d (T : measurableType d) (R : realType). Variables (mu : {sigma_finite_measure set T -> \bar R}) (nu : {finite_measure set T -> \bar R}). -Local Lemma radon_nikodym_sigma_finite : nu `<< mu -> - exists f : T -> \bar R, [/\ forall x, f x >= 0, mu.-integrable [set: T] f & - forall E, E \in measurable -> nu E = integral mu E f]. +Lemma radon_nikodym_sigma_finite : nu `<< mu -> + exists f : T -> \bar R, [/\ forall x, f x >= 0, forall x, f x \is a fin_num, + mu.-integrable [set: T] f & + forall A, measurable A -> nu A = \int[mu]_(x in A) f x]. Proof. -move=> nu_mu. -have [F TF mFAFfin] := sigma_finiteT mu. -have {mFAFfin}[mF Ffin] := all_and2 mFAFfin. +move=> nu_mu; have [F TF /all_and2[mF muFoo]] := sigma_finiteT mu. pose E := seqDU F. have mE k : measurable (E k). by apply: measurableD => //; exact: bigsetU_measurable. -have Efin k : mu (E k) < +oo. - by rewrite (le_lt_trans _ (Ffin k))// le_measure ?inE//; exact: subDsetl. -have bigcupE : \bigcup_i E i = setT by rewrite TF [RHS]seqDU_bigcup_eq. -have tE := @trivIset_seqDU _ F. +have muEoo k : mu (E k) < +oo. + by rewrite (le_lt_trans _ (muFoo k))// le_measure ?inE//; exact: subDsetl. +have UET : \bigcup_i E i = [set: T] by rewrite TF [RHS]seqDU_bigcup_eq. +have tE := trivIset_seqDU F. pose mu_ j : {finite_measure set T -> \bar R} := - [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (Efin j)]. -have H1 i : nu (E i) < +oo by rewrite ltey_eq fin_num_measure. + [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (muEoo j)]. +have nuEoo i : nu (E i) < +oo by rewrite ltey_eq fin_num_measure. pose nu_ j : {finite_measure set T -> \bar R} := - [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (H1 j)]. + [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (nuEoo j)]. have nu_mu_ k : nu_ k `<< mu_ k. by move=> S mS mu_kS0; apply: nu_mu => //; exact: measurableI. -have [g Hg] := choice (fun j => radon_nikodym_finite (nu_mu_ j)). -have [g_ge0 integrable_g int_gE {Hg}] := all_and3 Hg. -pose f_ j x := if x \in E j then g j x else 0. -have fRN_ge0 k x : 0 <= f_ k x by rewrite /f_; case: ifP. +have [g_] := choice (fun j => radon_nikodym_finite (nu_mu_ j)). +move=> /all_and3[g_ge0 ig_ int_gE]. +pose f_ j x := if x \in E j then g_ j x else 0. +have f_ge0 k x : 0 <= f_ k x by rewrite /f_; case: ifP. have mf_ k : measurable_fun setT (f_ k). apply: measurable_fun_if => //. - by apply: (measurable_fun_bool true); rewrite preimage_mem_true. - rewrite preimage_mem_true. - by apply: measurable_funTS => //; have /integrableP[] := integrable_g k. -have int_f_T k : integrable mu setT (f_ k). + by apply: measurable_funTS => //; have /integrableP[] := ig_ k. +have if_T k : integrable mu setT (f_ k). apply/integrableP; split => //. under eq_integral do rewrite gee0_abs//. rewrite -(setUv (E k)) integral_setU //; last 3 first. @@ -1560,7 +1559,7 @@ have int_f_E j S : measurable S -> \int[mu]_(x in S) f_ j x = nu (S `&` E j). rewrite -{1}(setUIDK S (E j)) (integral_setU _ mSIEj mSDEj)//; last 2 first. - by rewrite setUIDK; exact: (measurable_funS measurableT). - by apply/disj_set2P; rewrite setDE setIACA setICr setI0. - rewrite /f_ -(eq_integral _ (g j)); last first. + rewrite /f_ -(eq_integral _ (g_ j)); last first. by move=> x /[!inE] SIEjx; rewrite /f_ ifT// inE; exact: (@subIsetr _ S). rewrite (@eq_measure_integral _ _ _ (S `&` E j) (mu_ j)); last first. move=> A mA; rewrite subsetI => -[_ ?]; rewrite /mu_ /=. @@ -1576,53 +1575,45 @@ have int_f_nuT : \int[mu]_x f x = nu setT. rewrite integral_nneseries//. transitivity (\sum_(n i _; rewrite int_f_E// setTI. - rewrite -bigcupE measure_bigcup//. + rewrite -UET measure_bigcup//. by apply: eq_eseriesl => // x; rewrite in_setT. -exists f; split. -- by move=> t; rewrite /f; exact: nneseries_ge0. -- apply/integrableP; split; first exact: ge0_emeasurable_fun_sum. +have mf : measurable_fun setT f by exact: ge0_emeasurable_fun_sum. +have fi : mu.-integrable setT f. + apply/integrableP; split => //. under eq_integral do (rewrite gee0_abs; last exact: nneseries_ge0). by rewrite int_f_nuT ltey_eq fin_num_measure. -move=> A /[!inE] mA; rewrite integral_nneseries//; last first. - by move=> n; exact: measurable_funTS. -rewrite nneseries_esum; last by move=> m _; rewrite integral_ge0. -under eq_esum do rewrite int_f_E//. -rewrite -nneseries_esum; last first. - by move=> n; rewrite measure_ge0//; exact: measurableI. -rewrite (@eq_eseriesl _ _ (fun x => x \in [set: nat])); last first. - by move=> x; rewrite in_setT. -rewrite -measure_bigcup//. -- by rewrite -setI_bigcupr bigcupE setIT. -- by move=> i _; exact: measurableI. -- exact: trivIset_setIl. -Qed. - -Lemma radon_nikodym_sigma_finite_fin_num : nu `<< mu -> - exists f : T -> \bar R, [/\ forall x, f x >= 0, forall x, f x \is a fin_num, - mu.-integrable [set: T] f & - forall A, measurable A -> nu A = \int[mu]_(x in A) f x]. -Proof. -move=> /radon_nikodym_sigma_finite[f [f0 fi nuf]]. have ae_f := integrable_ae measurableT fi. -pose g x := if f x \is a fin_num then f x else 0. -have fg : ae_eq mu setT f g. +pose f' x := if f x \is a fin_num then f x else 0. +have ff' : ae_eq mu setT f f'. case: ae_f => N [mN N0 fN]; exists N; split => //. apply: subset_trans fN; apply: subsetC => z/= /(_ I) fz _. - by rewrite /g fz. -move/integrableP : fi => [mf fi]. -have mg : measurable_fun [set: T] g. + by rewrite /f' fz. +have mf' : measurable_fun setT f'. apply: measurable_fun_ifT => //; apply: (measurable_fun_bool true) => /=. by have := emeasurable_fin_num measurableT mf; rewrite setTI. -exists g; split => // [x|x| |A mA]. -- by rewrite /g; case: ifPn. -- by rewrite /g; case: ifPn. +exists f'; split. +- by move=> t; rewrite /f'; case: ifPn => // ?; exact: nneseries_ge0. +- by move=> t; rewrite /f'; case: ifPn. - apply/integrableP; split => //; apply/abse_integralP => //. - move/ae_eq_integral : (fg) => /(_ measurableT mf) <-//. - exact/abse_integralP. -- rewrite nuf ?inE//; apply: ae_eq_integral => //. - + exact: measurable_funTS. - + exact: measurable_funTS. - + exact: ae_eq_subset fg. + move/ae_eq_integral : (ff') => /(_ measurableT mf) <-//. + by apply/abse_integralP => //; move/integrableP : fi => []. +have nuf A : d.-measurable A -> nu A = \int[mu]_(x in A) f x. + move=> mA; rewrite integral_nneseries//; last first. + by move=> n; exact: measurable_funTS. + rewrite nneseries_esum; last by move=> m _; rewrite integral_ge0. + under eq_esum do rewrite int_f_E//. + rewrite -nneseries_esum; last first. + by move=> n; rewrite measure_ge0//; exact: measurableI. + rewrite (@eq_eseriesl _ _ (fun x => x \in [set: nat])); last first. + by move=> x; rewrite in_setT. + rewrite -measure_bigcup//. + - by rewrite -setI_bigcupr UET setIT. + - by move=> i _; exact: measurableI. + - exact: trivIset_setIl. +move=> A mA; rewrite nuf ?inE//; apply: ae_eq_integral => //. +- exact/measurable_funTS. +- exact/measurable_funTS. +- exact: ae_eq_subset ff'. Qed. End radon_nikodym_sigma_finite. @@ -1635,7 +1626,7 @@ Variables (nu : {finite_measure set T -> \bar R}) Definition f : T -> \bar R := match pselect (nu `<< mu) with - | left nu_mu => sval (cid (radon_nikodym_sigma_finite_fin_num nu_mu)) + | left nu_mu => sval (cid (radon_nikodym_sigma_finite nu_mu)) | right _ => cst -oo end. @@ -1783,10 +1774,10 @@ Local Lemma Radon_Nikodym0 : nu `<< mu -> forall A, measurable A -> nu A = \int[mu]_(x in A) f x]. Proof. move=> nu_mu; have [P [N nuPN]] := Hahn_decomposition nu. -have [fp [fp0 fpfin intfp fpE]] := @radon_nikodym_sigma_finite_fin_num _ _ _ mu +have [fp [fp0 fpfin intfp fpE]] := @radon_nikodym_sigma_finite _ _ _ mu [the {finite_measure set _ -> \bar _} of jordan_pos nuPN] (jordan_pos_dominates nuPN nu_mu). -have [fn [fn0 fnfin intfn fnE]] := @radon_nikodym_sigma_finite_fin_num _ _ _ mu +have [fn [fn0 fnfin intfn fnE]] := @radon_nikodym_sigma_finite _ _ _ mu [the {finite_measure set _ -> \bar _} of jordan_neg nuPN] (jordan_neg_dominates nuPN nu_mu). exists (fp \- fn); split; first by move=> x; rewrite fin_numB// fpfin fnfin. @@ -1802,7 +1793,7 @@ Definition Radon_Nikodym : T -> \bar R := | left nu_mu => sval (cid (Radon_Nikodym0 nu_mu)) | right _ => cst -oo end. - +xxx Lemma Radon_NikodymE (numu : nu `<< mu) : Radon_Nikodym = sval (cid (Radon_Nikodym0 numu)). Proof. diff --git a/theories/sequences.v b/theories/sequences.v index d47856e70..de8d8055a 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -257,6 +257,7 @@ by rewrite /seqDU -setIDA bigcup_mkord -big_distrr/= setDIr setIUr setDIK set0U. Qed. End seqDU. +Arguments trivIset_seqDU {T} F. #[global] Hint Resolve trivIset_seqDU : core. Section seqD.