From 4bddc61da9f6a13f7c6208e3f70048db47382608 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Thu, 26 Oct 2023 10:13:38 +0900 Subject: [PATCH 01/13] Radon_Nikodym chain rule Co-authored-by: IshiguroYoshihiro <103252572+IshiguroYoshihiro@users.noreply.github.com> --- theories/charge.v | 596 +++++++++++++++++++++++++++++------ theories/lebesgue_integral.v | 16 +- 2 files changed, 508 insertions(+), 104 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index 1fd90eb7b..d7f3fd87a 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -131,6 +131,7 @@ HB.instance Definition _ := HB.end. Section charge_lemmas. + Context d (T : ringOfSetsType d) (R : numFieldType). Implicit Type nu : {charge set T -> \bar R}. @@ -219,6 +220,29 @@ HB.instance Definition _ := isMeasure.Build _ T R (measure_of_charge nupos) End measure_of_charge. Arguments measure_of_charge {d T R}. +Definition charge_of_finite_measure d (T : measurableType d) (R : realType) + (mu : {finite_measure set T -> \bar R}) : set T -> \bar R := mu. + +Section charge_of_finite_measure. +Context d (T : measurableType d) (R : realType). +Variables (mu : {finite_measure set T -> \bar R}). + +Local Notation nu := (charge_of_finite_measure mu). + +Let nu0 : nu set0 = 0. Proof. exact: measure0. Qed. + +Let nu_finite S : measurable S -> nu S \is a fin_num. +Proof. by apply: fin_num_measure. Qed. + +Let nu_sigma_additive : semi_sigma_additive nu. +Proof. exact: measure_semi_sigma_additive. Qed. + +HB.instance Definition _ := isCharge.Build _ T R (charge_of_finite_measure mu) + nu0 nu_finite nu_sigma_additive. + +End charge_of_finite_measure. +Arguments charge_of_finite_measure {d T R}. + Section charge_lemmas_realFieldType. Context d (T : ringOfSetsType d) (R : realFieldType). Implicit Type nu : {charge set T -> \bar R}. @@ -368,8 +392,16 @@ Qed. HB.instance Definition _ := isCharge.Build _ _ _ cscale cscale0 cscale_finite_measure_function cscale_sigma_additive. +Lemma cscaleE A : cscale A = r%:E * nu A. Proof. by []. Qed. + End charge_scale. +Lemma dominates_cscale d (T : measurableType d) (R : realType) + (mu : {sigma_finite_measure set T -> \bar R}) + (nu : {charge set T -> \bar R}) + (c : R) : nu `<< mu -> cscale c nu `<< mu. +Proof. by move=> numu E mE /numu; rewrite /cscale => ->//; rewrite mule0. Qed. + Section charge_add. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). @@ -400,8 +432,72 @@ Qed. HB.instance Definition _ := isCharge.Build _ _ _ cadd cadd0 cadd_finite cadd_sigma_additive. +Lemma caddE E : cadd E = m1 E + m2 E. Proof. by []. Qed. + End charge_add. +Lemma dominates_caddl d (T : measurableType d) + (R : realType) (mu : {sigma_finite_measure set T -> \bar R}) + (nu0 nu1 : {charge set T -> \bar R}) : + nu0 `<< mu -> nu1 `<< mu -> + cadd nu0 nu1 `<< mu. +Proof. +by move=> nu0mu nu1mu A mA A0; rewrite /cadd nu0mu// nu1mu// adde0. +Qed. + +Section pushforward_charge. +Local Open Scope ereal_scope. +Context d d' (T1 : measurableType d) (T2 : measurableType d') (f : T1 -> T2). +Variables (R : realFieldType) (nu : {charge set T1 -> \bar R}). + +Definition cpushforward (mf : measurable_fun setT f) A := nu (f @^-1` A). + +Hypothesis mf : measurable_fun setT f. + +Let cpushforward0 : cpushforward mf set0 = 0. +Proof. by rewrite /cpushforward preimage_set0 charge0. Qed. + +Let cpushforward_finite A : measurable A -> cpushforward mf A \is a fin_num. +Proof. +move=> mA; apply: fin_num_measure. +by rewrite -[X in measurable X]setTI; apply: mf. +Qed. + +Let cpushforward_sigma_additive : semi_sigma_additive (cpushforward mf). +Proof. +move=> F mF tF mUF; rewrite /cpushforward preimage_bigcup. +apply: charge_semi_sigma_additive. +- by move=> n; rewrite -[X in measurable X]setTI; exact: mf. +- apply/trivIsetP => /= i j _ _ ij; rewrite -preimage_setI. + by move/trivIsetP : tF => /(_ _ _ _ _ ij) ->//; rewrite preimage_set0. +- by rewrite -preimage_bigcup -[X in measurable X]setTI; exact: mf. +Qed. + +HB.instance Definition _ := isCharge.Build _ _ _ + (cpushforward mf) cpushforward0 cpushforward_finite cpushforward_sigma_additive. + +End pushforward_charge. + +HB.builders Context d (T : measurableType d) (R : realType) + mu of Measure_isFinite d T R mu. + +HB.instance Definition _ := isCharge.Build _ _ _ + mu (measure0 [the content _ _ of mu]) fin_num_measure measure_semi_sigma_additive. + +HB.end. + +Section dominates_pushforward. + +Lemma dominates_pushforward d d' (T : measurableType d) (T' : measurableType d') + (R : realType) (mu : {sigma_finite_measure set T -> \bar R}) + (nu : {charge set T -> \bar R}) (f : T -> T') (mf : measurable_fun setT f) : + nu `<< mu -> cpushforward nu mf `<< pushforward mu mf. +Proof. +by move=> numu A mA; apply: numu; rewrite -[X in measurable X]setTI; exact: mf. +Qed. + +End dominates_pushforward. + Section positive_negative_set. Context d (T : semiRingOfSetsType d) (R : numDomainType). Implicit Types nu : set T -> \bar R. @@ -822,17 +918,23 @@ Let mP : measurable P. Proof. by have [[mP _] _ _ _] := nuPN. Qed. Let mN : measurable N. Proof. by have [_ [mN _] _ _] := nuPN. Qed. -Let cjordan_pos : {charge set T -> \bar R} := [the charge _ _ of crestr0 nu mP]. +Local Definition cjordan_pos : {charge set T -> \bar R} := [the charge _ _ of crestr0 nu mP]. + +Lemma cjordan_posE A : cjordan_pos A = crestr0 nu mP A. +Proof. by []. Qed. Let positive_set_cjordan_pos E : 0 <= cjordan_pos E. Proof. have [posP _ _ _] := nuPN. -rewrite /cjordan_pos/= /crestr0/=; case: ifPn => // /[1!inE] mE. +rewrite cjordan_posE /crestr0/=; case: ifPn => // /[1!inE] mE. by apply posP; [apply: measurableI|apply: subIsetr]. Qed. Definition jordan_pos := measure_of_charge _ positive_set_cjordan_pos. +Lemma jordan_posE A : jordan_pos A = cjordan_pos A. +Proof. by []. Qed. + HB.instance Definition _ := Measure.on jordan_pos. Let finite_jordan_pos : fin_num_fun jordan_pos. @@ -841,18 +943,24 @@ Proof. by move=> U mU; rewrite fin_num_measure. Qed. HB.instance Definition _ := @Measure_isFinite.Build _ _ _ jordan_pos finite_jordan_pos. -Let cjordan_neg : {charge set T -> \bar R} := +Local Definition cjordan_neg : {charge set T -> \bar R} := [the charge _ _ of cscale (-1) [the charge _ _ of crestr0 nu mN]]. +Lemma cjordan_negE A : cjordan_neg A = - crestr0 nu mN A. +Proof. by rewrite /= cscaleE EFinN mulN1e. Qed. + Let positive_set_cjordan_neg E : 0 <= cjordan_neg E. Proof. -rewrite /cjordan_neg/= /cscale/= /crestr0/= muleC mule_le0//. -case: ifPn => // /[1!inE] mE. +rewrite cjordan_negE /crestr0/=; case: ifPn => // /[1!inE] mE. +rewrite /crestr lee_oppr oppe0. by move: nuPN => [_ [_ +] _ _] => -> //; exact: measurableI. Qed. Definition jordan_neg := measure_of_charge _ positive_set_cjordan_neg. +Lemma jordan_negE A : jordan_neg A = cjordan_neg A. +Proof. by []. Qed. + HB.instance Definition _ := Measure.on jordan_neg. Let finite_jordan_neg : fin_num_fun jordan_neg. @@ -861,12 +969,12 @@ Proof. by move=> U mU; rewrite fin_num_measure. Qed. HB.instance Definition _ := @Measure_isFinite.Build _ _ _ jordan_neg finite_jordan_neg. -Lemma jordan_decomp A : measurable A -> nu A = jordan_pos A - jordan_neg A. +Lemma jordan_decomp (A : set T) (mA : measurable A) : + nu A = (cadd [the charge _ _ of jordan_pos] [the charge _ _ of (cscale (-1) [the charge _ _ of jordan_neg])]) A. Proof. -move=> mA; rewrite /jordan_pos /jordan_neg/= /measure_of_charge/=. -rewrite /cscale/= /crestr0/= mem_set// -[in LHS](setIT A). +rewrite caddE cjordan_posE /= cscaleE EFinN mulN1e cjordan_negE oppeK. +rewrite /crestr0 mem_set// -[in LHS](setIT A). case: nuPN => _ _ <- PN0; rewrite setIUr chargeU//. -- by rewrite EFinN mulN1e oppeK. - exact: measurableI. - exact: measurableI. - by rewrite setIACA PN0 setI0. @@ -876,23 +984,20 @@ Lemma jordan_pos_dominates (mu : {measure set T -> \bar R}) : nu `<< mu -> jordan_pos `<< mu. Proof. move=> nu_mu A mA muA0; have := nu_mu A mA muA0. -rewrite jordan_decomp// /jordan_pos /jordan_neg /measure_of_charge/=. -rewrite /cscale/= /crestr0/= mem_set// EFinN mulN1e oppeK. +rewrite jordan_posE// cjordan_posE /crestr0 mem_set// /crestr/=. have mAP : measurable (A `&` P) by exact: measurableI. -suff : mu (A `&` P) = 0 by move/(nu_mu _ mAP); rewrite /crestr => ->. -by apply/eqP; rewrite -measure_le0 -muA0 le_measure// inE. +suff : mu (A `&` P) = 0 by move/(nu_mu _ mAP) => ->. +by apply/eqP; rewrite eq_le measure_ge0// andbT -muA0 le_measure// inE. Qed. Lemma jordan_neg_dominates (mu : {measure set T -> \bar R}) : nu `<< mu -> jordan_neg `<< mu. Proof. move=> nu_mu A mA muA0; have := nu_mu A mA muA0. -rewrite jordan_decomp// /jordan_pos /jordan_neg /measure_of_charge/=. -rewrite /cscale/= /crestr0/= mem_set//. +rewrite jordan_negE// cjordan_negE /crestr0 mem_set// /crestr/=. have mAN : measurable (A `&` N) by exact: measurableI. -suff : mu (A `&` N) = 0. - by move=> /(nu_mu _ mAN); rewrite /crestr => ->; rewrite mule0. -by apply/eqP; rewrite -measure_le0 -muA0 le_measure// inE. +suff : mu (A `&` N) = 0 by move=> /(nu_mu _ mAN) ->; rewrite oppe0. +by apply/eqP; rewrite eq_le measure_ge0// andbT -muA0 le_measure// inE. Qed. End jordan_decomposition. @@ -1436,15 +1541,30 @@ Qed. End radon_nikodym_finite. -Section radon_nikodym. +(* TODO: move? *) +Lemma measure_dominates_ae_eq d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (nu : {measure set T -> \bar R}) + (f g : T -> \bar R) E : measurable E -> + nu `<< mu -> ae_eq mu E f g -> ae_eq nu E f g. +Proof. by move=> mE munu [A [mA A0 EA]]; exists A; split => //; exact: munu. Qed. + +(* TODO: move *) +Lemma ae_eqS d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) A B f g : + B `<=` A -> ae_eq mu A f g -> ae_eq mu B f g. +Proof. +move=> BA. +case => N [mN N0 fg]; exists N; split => //. +by apply: subset_trans fg; apply: subsetC => z /= /[swap] /BA ? ->//. +Qed. + +Section radon_nikodym_sigma_finite. Context d (T : measurableType d) (R : realType). +Variables (mu : {sigma_finite_measure set T -> \bar R}) + (nu : {finite_measure set T -> \bar R}). -Let radon_nikodym_sigma_finite - (mu : {sigma_finite_measure set T -> \bar R}) - (nu : {finite_measure set T -> \bar R}) : - nu `<< mu -> - exists2 f : T -> \bar R, mu.-integrable [set: T] f & - forall E, E \in measurable -> nu E = integral mu E f. +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]. Proof. move=> nu_mu. have [F TF mFAFfin] := sigma_finiteT mu. @@ -1512,120 +1632,400 @@ have int_f_nuT : \int[mu]_x f x = nu setT. by apply: eq_eseriesr => i _; rewrite int_f_E// setTI. rewrite -bigcupE measure_bigcup//. by apply: eq_eseriesl => // x; rewrite in_setT. -exists f. - apply/integrableP; split; first exact: ge0_emeasurable_fun_sum. +exists f; split. +- by move=> t; rewrite /f; exact: nneseries_ge0. +- apply/integrableP; split; first exact: ge0_emeasurable_fun_sum. 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. - -Let Radon_Nikodym0 - (mu : {sigma_finite_measure set T -> \bar R}) (nu : {charge set T -> \bar R}) : - nu `<< mu -> - exists2 f : T -> \bar R, mu.-integrable [set: T] f & +- 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. + 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. + apply: measurable_fun_ifT => //; apply: (measurable_fun_bool true) => /=. + by have := emeasurable_fin_num measurableT mf; rewrite setTI. +exists g; split => //. +- by move=> x; rewrite /g; case: ifPn. +- by move=> x; rewrite /g; case: ifPn. +- apply/integrableP; split => //; apply/abse_integralP => //. + move/ae_eq_integral : (fg) => /(_ measurableT mf) <-//. + exact/abse_integralP. +- move=> A mA; rewrite nuf ?inE//; apply: ae_eq_integral => //. + + exact: measurable_funTS. + + exact: measurable_funTS. + + exact: ae_eqS fg. +Qed. + +End radon_nikodym_sigma_finite. + +Module Radon_Nikodym_SigmaFinite. +Section radon_nikodym_sigma_finite_def. +Context d (T : measurableType d) (R : realType). +Variables (nu : {finite_measure set T -> \bar R}) + (mu : {sigma_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)) + | right _ => cst -oo + end. + +Theorem f_ge0 : nu `<< mu -> forall x, 0 <= f x. +Proof. +by move=> numu; rewrite /f; case: pselect => // {}numu; case: cid => x []. +Qed. + +Theorem f_fin_num : nu `<< mu -> forall x, f x \is a fin_num. +Proof. +by move=> numu; rewrite /f; case: pselect => // {}numu; case: cid => x []. +Qed. + +Theorem f_integrable : nu `<< mu -> mu.-integrable [set: T] f. +Proof. +by move=> numu; rewrite /f; case: pselect => // {}numu; case: cid => x []. +Qed. + +Theorem f_integral : nu `<< mu -> forall A, measurable A -> + nu A = \int[mu]_(x in A) f x. +Proof. +by move=> numu; rewrite /f; case: pselect => // {}numu; case: cid => x []. +Qed. + +End radon_nikodym_sigma_finite_def. + +Section integrableM. +Context d (T : measurableType d) (R : realType). +Variables (nu : {finite_measure set T -> \bar R}) + (mu : {sigma_finite_measure set T -> \bar R}). +Hypothesis numu : nu `<< mu. +Implicit Types f : T -> \bar R. + +Local Notation "'d nu '/d mu" := (f nu mu). + +Lemma change_of_variables f : (forall x, 0 <= f x) -> + forall E, measurable E -> measurable_fun E f -> + \int[mu]_(x in E) (f x * ('d nu '/d mu) x) = \int[nu]_(x in E) f x. +Proof. +move=> f0 E mE mf; set g := 'd nu '/d mu. +have [h [ndh hf]] := approximation mE mf (fun x _ => f0 x). +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. + under eq_integral. by move=> x /[!inE] Ex; rewrite fE //; over. + apply: monotone_convergence => //. + - move=> n; apply/EFin_measurable_fun. + 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. +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]. + under eq_integral. by move=> x /[!inE] Ex; rewrite fg //; over. + apply: monotone_convergence => [//| | |]. + - move=> n; apply/emeasurable_funM; apply/measurable_funTS. + exact/EFin_measurable_fun. + 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. +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. + under eq_fun. by move=> n; rewrite suf; over. by []. +transitivity (\int[nu]_(x in E) + (\sum_(y \in range (h n)) (y * \1_(h n @^-1` [set y]) x)%:E)); last first. + by apply: eq_integral => t tE; rewrite /= fimfunE -fsumEFin. +have indich m r : measurable_fun E (fun x => (r * \1_(h m @^-1` [set r]) x)%:E). + by apply: (measurable_comp measurableT) => //; exact: measurable_funM. +rewrite ge0_integral_fsum//; last by move=> m y Ey; exact: nnfun_muleindic_ge0. +transitivity (\int[mu]_(x in E) (\sum_(y \in range (h n)) + (y * \1_(h n @^-1` [set y]) x)%:E * g x)). + under [RHS]eq_integral => x xE. + rewrite -ge0_mule_fsuml; last first. + by move=> y; exact: nnfun_muleindic_ge0. + rewrite fsumEFin // -(fimfunE _ x); over. + by []. +rewrite ge0_integral_fsum//; last 2 first. + - move=> y; apply: emeasurable_funM => //; apply: measurable_funTS. + exact: measurable_int (f_integrable _). + - by move=> m y Ey; rewrite mule_ge0//; [exact: nnfun_muleindic_ge0| + exact: f_ge0]. +apply: eq_fsbigr => r rhn. +under [RHS]eq_integral do rewrite EFinM. +rewrite integralZl_indic_nnsfun => //. +under [LHS]eq_integral do rewrite EFinM -muleA. +rewrite ge0_integralZl//. + suff intE1 F : measurable F -> \int[nu]_(x in E) (EFin \o \1_F) x = + \int[mu]_(x in E) ((EFin \o \1_F) x * g x). + by rewrite intE1. + move=> mF /=. + under eq_integral. + by move=> x xE; rewrite -[_%:E]mul1e -/(idfun 1); over. + rewrite -(integral_setI_indic _ _)//. + transitivity (\int[mu]_(x in E `&` F) g x). + rewrite -f_integral//=; last exact: measurableI. + by rewrite integral_cst ?mul1e//; exact: measurableI. + by rewrite integral_setI_indic//; under eq_integral do rewrite muleC. +- apply: emeasurable_funM; first exact/EFin_measurable_fun. + by apply: measurable_funTS => //; exact: measurable_int (f_integrable _). +- by move=> t Et; rewrite mule_ge0// ?lee_fin//; exact: f_ge0. +- by move: rhn; rewrite inE => -[t _ <-]; rewrite lee_fin. +Qed. + +Lemma integrableM f : (forall x, 0 <= f x) -> forall E, measurable E -> + nu.-integrable E f -> mu.-integrable E (f \* 'd nu '/d mu). +Proof. +move=> f0 E mE intEf; apply/integrableP; split. + apply: emeasurable_funM; first exact: (@measurable_int _ _ _ nu). + by apply: measurable_funTS; exact: measurable_int (f_integrable _). +under eq_integral. + move=> x _; rewrite gee0_abs; last first. + by apply: mule_ge0=> //; exact: f_ge0. + over. +rewrite change_of_variables//; last exact: (@measurable_int _ _ _ nu). +by move/integrableP : intEf=> [mf +]; under eq_integral do rewrite gee0_abs//. +Qed. + +End integrableM. + +Section chain_rule. +Context d (T : measurableType d) (R : realType). +Variables (nu : {finite_measure set T -> \bar R}) + (la : {sigma_finite_measure set T -> \bar R}) + (mu : {finite_measure set T -> \bar R}). + +Local Notation "'d nu '/d mu" := (f nu mu). + +Lemma chain_rule : nu `<< mu -> mu `<< la -> forall E, measurable E -> + ae_eq la E ('d nu '/d la) ('d nu '/d mu \* 'd mu '/d la). +Proof. +move=> numu mula E mE; have nula := measure_dominates_trans numu mula. +have mf : measurable_fun E ('d nu '/d mu). + by apply: measurable_funTS; exact: measurable_int (f_integrable _). +have [h [ndh hf]] := approximation mE mf (fun x _ => f_ge0 numu x). +apply: integral_ae_eq => //. +- apply: (integrableS measurableT) => //. + apply: f_integrable. + exact: (measure_dominates_trans numu mula). +- apply: emeasurable_funM => //; apply: measurable_funTS. + exact: measurable_int (f_integrable _). +- move=> A AE mA; rewrite change_of_variables//. + + by rewrite -!f_integral. + + exact: f_ge0. + + exact: measurable_funS mf. +Qed. + +End chain_rule. +End Radon_Nikodym_SigmaFinite. + +Section radon_nikodym. +Context d (T : measurableType d) (R : realType). +Variables (nu : {charge set T -> \bar R}) + (mu : {sigma_finite_measure set T -> \bar R}). + +Local Lemma Radon_Nikodym0 : nu `<< mu -> + exists2 f : T -> \bar R, (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 [P [N nuPN]] := Hahn_decomposition nu. -have [fp intfp fpE] := @radon_nikodym_sigma_finite mu +have [fp [fp0 fpfin intfp fpE]] := @radon_nikodym_sigma_finite_fin_num _ _ _ mu [the {finite_measure set _ -> \bar _} of jordan_pos nuPN] (jordan_pos_dominates nuPN nu_mu). -have [fn intfn fnE] := @radon_nikodym_sigma_finite mu +have [fn [fn0 fnfin intfn fnE]] := @radon_nikodym_sigma_finite_fin_num _ _ _ mu [the {finite_measure set _ -> \bar _} of jordan_neg nuPN] (jordan_neg_dominates nuPN nu_mu). -exists (fp \- fn); first exact: integrableB. -move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//. -- by rewrite -fpE ?inE// -fnE ?inE. -- exact: (integrableS measurableT). -- exact: (integrableS measurableT). +exists (fp \- fn); first by move=> x; rewrite fin_numB// fpfin fnfin. +split; first exact: integrableB. +move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//; + [|exact: (integrableS measurableT)..]. +rewrite -fpE ?inE// -fnE ?inE//= caddE jordan_posE jordan_negE. +by rewrite [X in _ + X]/= cscaleE EFinN mulN1e. Qed. -Definition Radon_Nikodym - (mu : {sigma_finite_measure set T -> \bar R}) - (nu : {charge set T -> \bar R}) : T -> \bar R := +Definition Radon_Nikodym : T -> \bar R := match pselect (nu `<< mu) with | left nu_mu => sval (cid2 (Radon_Nikodym0 nu_mu)) | right _ => cst -oo end. -Local Notation "'d nu '/d mu" := (Radon_Nikodym mu nu). +Lemma Radon_NikodymE (numu : nu `<< mu) : + Radon_Nikodym = sval (cid2 (Radon_Nikodym0 numu)). +Proof. +rewrite /= /Radon_Nikodym; case: pselect => //= numu'. +by congr (sval (cid2 (Radon_Nikodym0 _))); exact: Prop_irrelevance. +Qed. -Theorem Radon_Nikodym_integrable - (mu : {sigma_finite_measure set T -> \bar R}) - (nu : {charge set T -> \bar R}) : - nu `<< mu -> - mu.-integrable [set: T] ('d nu '/d mu). +Theorem Radon_Nikodym_fin_num : nu `<< mu -> + forall x, Radon_Nikodym x \is a fin_num. Proof. move=> numu; rewrite /Radon_Nikodym; case: pselect => // {}numu. by case: cid2. Qed. -Theorem Radon_Nikodym_integral - (mu : {sigma_finite_measure set T -> \bar R}) - (nu : {charge set T -> \bar R}) : - nu `<< mu -> - forall A, measurable A -> nu A = \int[mu]_(x in A) ('d nu '/d mu) x. +Theorem Radon_Nikodym_integrable : nu `<< mu -> + mu.-integrable [set: T] Radon_Nikodym. Proof. move=> numu; rewrite /Radon_Nikodym; case: pselect => // {}numu. -by case: cid2. +by case: cid2 => ? ? []. +Qed. + +Theorem Radon_Nikodym_integral : nu `<< mu -> + forall A, measurable A -> nu A = \int[mu]_(x in A) Radon_Nikodym x. +Proof. +move=> numu; rewrite /Radon_Nikodym; case: pselect => // {}numu. +by case: cid2 => ? ? []. Qed. End radon_nikodym. -Notation "'d nu '/d mu" := (Radon_Nikodym mu nu) : charge_scope. +Notation "'d nu '/d mu" := (Radon_Nikodym nu mu) : charge_scope. -Section radon_nikodym_lemmas. +#[global] Hint Extern 0 (_.-integrable setT ('d _ '/d _)) => + solve [apply: Radon_Nikodym_integrable] : core. +#[global] Hint Extern 0 (measurable_fun setT ('d _ '/d _)) => + solve [apply: measurable_int; exact: Radon_Nikodym_integrable] : core. + +Section Radon_Nikodym_charge_of_finite_measure. Context d (T : measurableType d) (R : realType). +Variables (nu : {finite_measure set T -> \bar R}) + (mu : {sigma_finite_measure set T -> \bar R}). +Hypothesis numu : nu `<< mu. + +Lemma ae_eq_Radon_Nikodym_SigmaFinite E : measurable E -> + ae_eq mu E (Radon_Nikodym_SigmaFinite.f nu mu) + ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu). +Proof. +move=> mE; apply: integral_ae_eq => //. +- apply: (integrableS measurableT) => //. + exact: Radon_Nikodym_SigmaFinite.f_integrable. +- exact: measurable_funTS. +- move=> A AE mA; rewrite -Radon_Nikodym_integral//. + by rewrite -Radon_Nikodym_SigmaFinite.f_integral. +Qed. -Lemma dominates_cscale (mu : {sigma_finite_measure set T -> \bar R}) - (nu : {charge set T -> \bar R}) (c : R) : - nu `<< mu -> cscale c nu `<< mu. -Proof. by move=> numu E mE /numu; rewrite /cscale => ->//; rewrite mule0. Qed. +End Radon_Nikodym_charge_of_finite_measure. -Lemma Radon_Nikodym_cscale (mu : {sigma_finite_measure set T -> \bar R}) - (nu : {charge set T -> \bar R}) (c : R) : - nu `<< mu -> - ae_eq mu [set: T] ('d [the charge _ _ of cscale c nu] '/d mu) - (fun x => c%:E * 'd nu '/d mu x). +Section Radon_Nikodym_change_of_variables. +Context d (T : measurableType d) (R : realType). +Variables (nu : {finite_measure set T -> \bar R}) + (mu : {sigma_finite_measure set T -> \bar R}). +Hypothesis numu : nu `<< mu. +Implicit Types f : T -> \bar R. + +Lemma Radon_Nikodym_change_of_variables f E : measurable E -> + nu.-integrable E f -> + \int[mu]_(x in E) (f x * ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu) x) = + \int[nu]_(x in E) f x. +Proof. +move=> mE mf; rewrite [in RHS](funeposneg f) integralB //; last 2 first. + - exact: integrable_funepos. + - exact: integrable_funeneg. +transitivity (\int[mu]_(x in E) (f \* (Radon_Nikodym_SigmaFinite.f nu mu)) x). + apply: ae_eq_integral => //. + - apply: emeasurable_funM => //; last exact: measurable_funTS. + exact: measurable_int mf. + - apply: emeasurable_funM => //; first exact: measurable_int mf. + apply: measurable_funTS. + exact: measurable_int (Radon_Nikodym_SigmaFinite.f_integrable _). + - exact/ae_eq_mul2l/ae_eq_sym/ae_eq_Radon_Nikodym_SigmaFinite. +transitivity (\int[mu]_(x in E) (f^\+ \* (Radon_Nikodym_SigmaFinite.f nu mu) \- + f^\- \* (Radon_Nikodym_SigmaFinite.f nu mu)) x). + apply: eq_integral => x /[!inE] Ex. + rewrite [in LHS](funeposneg f) muleBl//=. + - exact: Radon_Nikodym_SigmaFinite.f_fin_num. + - exact: add_def_funeposneg. +rewrite [in LHS]integralB //; last 2 first. +- apply: Radon_Nikodym_SigmaFinite.integrableM => //. + exact: integrable_funepos. +- apply: Radon_Nikodym_SigmaFinite.integrableM => //. + exact: integrable_funeneg. +congr (_ - _). +- rewrite Radon_Nikodym_SigmaFinite.change_of_variables//. + by apply: measurable_int; exact: integrable_funepos mf. +- rewrite Radon_Nikodym_SigmaFinite.change_of_variables//. + by apply: measurable_int; exact: integrable_funeneg mf. +Qed. + +End Radon_Nikodym_change_of_variables. + +Section radon_nikodym_lemmas. +Context d (T : measurableType d) (R : realType). +Implicit Types (nu : {charge set T -> \bar R}) + (mu : {sigma_finite_measure set T -> \bar R}). + +Lemma Radon_Nikodym_cscale mu nu c E : measurable E -> nu `<< mu -> + ae_eq mu E ('d [the charge _ _ of cscale c nu] '/d mu) + (fun x => c%:E * 'd nu '/d mu x). Proof. -move=> numu; apply: integral_ae_eq => [//| | |E mE]. -- by apply: Radon_Nikodym_integrable; exact: dominates_cscale. - apply: emeasurable_funM => //. - exact: measurable_int (Radon_Nikodym_integrable _). +move=> mE numu; apply: integral_ae_eq => [//| | |A AE mA]. +- apply: (integrableS measurableT) => //. + by apply: Radon_Nikodym_integrable => /=; exact: dominates_cscale. +- by apply: measurable_funTS; exact: emeasurable_funM. - rewrite integralZl//; last first. by apply: (integrableS measurableT) => //; exact: Radon_Nikodym_integrable. rewrite -Radon_Nikodym_integral => //; last exact: dominates_cscale. by rewrite -Radon_Nikodym_integral. Qed. -Lemma dominates_caddl (mu : {sigma_finite_measure set T -> \bar R}) - (nu0 nu1 : {charge set T -> \bar R}) : - nu0 `<< mu -> nu1 `<< mu -> cadd nu0 nu1 `<< mu. -Proof. -by move=> nu0mu nu1mu A mA A0; rewrite /cadd nu0mu// nu1mu// adde0. -Qed. - -Lemma Radon_Nikodym_cadd (mu : {sigma_finite_measure set T -> \bar R}) - (nu0 nu1 : {charge set T -> \bar R}) : +Lemma Radon_Nikodym_cadd mu nu0 nu1 E : measurable E -> nu0 `<< mu -> nu1 `<< mu -> - ae_eq mu [set: T] ('d [the charge _ _ of cadd nu0 nu1] '/d mu) - ('d nu0 '/d mu \+ 'd nu1 '/d mu). -Proof. -move=> nu0mu nu1mu; apply: integral_ae_eq => [//| | |E mE]. -- by apply: Radon_Nikodym_integrable => /=; exact: dominates_caddl. - by apply: emeasurable_funD; exact: measurable_int (Radon_Nikodym_integrable _). -- rewrite integralD => //; [|exact: integrableS (Radon_Nikodym_integrable _)..]. + ae_eq mu E ('d [the charge _ _ of cadd nu0 nu1] '/d mu) + ('d nu0 '/d mu \+ 'd nu1 '/d mu). +Proof. +move=> mE nu0mu nu1mu; apply: integral_ae_eq => [//| | |A AE mA]. +- apply: (integrableS measurableT) => //. + by apply: Radon_Nikodym_integrable => /=; exact: dominates_caddl. +- by apply: measurable_funTS => //; exact: emeasurable_funD. +- rewrite integralD //; [|exact: integrableS (Radon_Nikodym_integrable _)..]. rewrite -Radon_Nikodym_integral //=; last exact: dominates_caddl. by rewrite -Radon_Nikodym_integral // -Radon_Nikodym_integral. Qed. End radon_nikodym_lemmas. + +Section Radon_Nikodym_chain_rule. +Context d (T : measurableType d) (R : realType). +Variables (nu : {charge set T -> \bar R}) + (la : {sigma_finite_measure set T -> \bar R}) + (mu : {finite_measure set T -> \bar R}). + +Lemma Radon_Nikodym_chain_rule : nu `<< mu -> mu `<< la -> + ae_eq la setT ('d nu '/d la) + ('d nu '/d mu \* 'd [the charge _ _ of charge_of_finite_measure mu] '/d la). +Proof. +have [Pnu [Nnu nuPN]] := Hahn_decomposition nu. +move=> numu mula; have nula := measure_dominates_trans numu mula. +apply: integral_ae_eq => //. +- exact: Radon_Nikodym_integrable. +- exact: emeasurable_funM. +- move=> E _ mE. + rewrite -Radon_Nikodym_integral// Radon_Nikodym_change_of_variables//. + + exact: Radon_Nikodym_integral. + + by apply: (integrableS measurableT) => //; exact: Radon_Nikodym_integrable. +Qed. + +End Radon_Nikodym_chain_rule. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 4bc3cc799..0f8301973 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4285,7 +4285,8 @@ Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) Let integral_measure_lt (D : set T) (mD : measurable D) (g f : T -> \bar R) : mu.-integrable D f -> mu.-integrable D g -> - (forall E, measurable E -> \int[mu]_(x in E) f x = \int[mu]_(x in E) g x) -> + (forall E, E `<=` D -> measurable E -> + \int[mu]_(x in E) f x = \int[mu]_(x in E) g x) -> mu (D `&` [set x | g x < f x]) = 0. Proof. move=> itf itg fg; pose E j := D `&` [set x | f x - g x >= j.+1%:R^-1%:E]. @@ -4300,7 +4301,8 @@ have muE j : mu (E j) = 0. rewrite integralB//; last 2 first. by apply: integrableS itf => //; exact: subIsetl. by apply: integrableS itg => //; exact: subIsetl. - rewrite fg// subee// fin_num_abs (le_lt_trans (le_abse_integral _ _ _))//. + rewrite fg//; last apply: subIsetl. + rewrite subee// fin_num_abs (le_lt_trans (le_abse_integral _ _ _))//. by apply: measurable_funS msg => //; first exact: subIsetl. apply: le_lt_trans (integrableP _ _ _ itg).2; apply: subset_integral => //. exact: measurableT_comp msg. @@ -4318,7 +4320,7 @@ have muE j : mu (E j) = 0. have nd_E : {homo E : n0 m / (n0 <= m)%N >-> (n0 <= m)%O}. move=> i j ij; apply/subsetPset => x [Dx /= ifg]; split => //. by move: ifg; apply: le_trans; rewrite lee_fin lef_pinv// ?posrE// ler_nat. -rewrite set_lte_bigcup. +rewrite real_interval.set_lte_bigcup. have /cvg_lim h1 : mu \o E --> 0 by apply: cvg_near_cst; exact: nearW. have := @nondecreasing_cvg_mu _ _ _ mu E mE (bigcupT_measurable E mE) nd_E. by move/cvg_lim => h2; rewrite setI_bigcupr -h2// h1. @@ -4326,15 +4328,17 @@ Qed. Lemma integral_ae_eq (D : set T) (mD : measurable D) (g f : T -> \bar R) : mu.-integrable D f -> measurable_fun D g -> - (forall E, measurable E -> \int[mu]_(x in E) f x = \int[mu]_(x in E) g x) -> + (forall E, E `<=` D -> measurable E -> + \int[mu]_(x in E) f x = \int[mu]_(x in E) g x) -> ae_eq mu D f g. Proof. move=> fi mg fg; have mf := measurable_int fi; have gi : mu.-integrable D g. apply/integrableP; split => //; apply/abse_integralP => //; rewrite -fg//. by apply/abse_integralP => //; case/integrableP : fi. -have mugf : mu (D `&` [set x | g x < f x]) = 0 by exact: integral_measure_lt. +have mugf : mu (D `&` [set x | g x < f x]) = 0. + by apply: integral_measure_lt. have mufg : mu (D `&` [set x | f x < g x]) = 0. - by apply: integral_measure_lt => // E mE; rewrite fg. + by apply: integral_measure_lt => // E ED mE; rewrite fg. have h : ~` [set x | D x -> f x = g x] = D `&` [set x | f x != g x]. apply/seteqP; split => [x/= /not_implyP[? /eqP]//|x/= [Dx fgx]]. by apply/not_implyP; split => //; exact/eqP. From f849d9a2c8cecd58b83c682aed7ba1033c1636a3 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Tue, 14 Nov 2023 16:40:50 +0900 Subject: [PATCH 02/13] fix --- theories/charge.v | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index d7f3fd87a..ef660d002 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -479,7 +479,10 @@ HB.instance Definition _ := isCharge.Build _ _ _ End pushforward_charge. HB.builders Context d (T : measurableType d) (R : realType) - mu of Measure_isFinite d T R mu. + (mu : set T -> \bar R) of Measure_isFinite d T R mu. + +Let mu0 : mu set0 = 0. +Proof. by apply: measure0. Qed. HB.instance Definition _ := isCharge.Build _ _ _ mu (measure0 [the content _ _ of mu]) fin_num_measure measure_semi_sigma_additive. @@ -970,7 +973,8 @@ HB.instance Definition _ := @Measure_isFinite.Build _ _ _ jordan_neg finite_jordan_neg. Lemma jordan_decomp (A : set T) (mA : measurable A) : - nu A = (cadd [the charge _ _ of jordan_pos] [the charge _ _ of (cscale (-1) [the charge _ _ of jordan_neg])]) A. + nu A = (cadd [the charge _ _ of jordan_pos] + ([the charge _ _ of cscale (-1) [the charge _ _ of jordan_neg]])) A. Proof. rewrite caddE cjordan_posE /= cscaleE EFinN mulN1e cjordan_negE oppeK. rewrite /crestr0 mem_set// -[in LHS](setIT A). From ad35771cbd000ee712ea28c02439295675cb8c4d Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Fri, 17 Nov 2023 18:01:22 +0900 Subject: [PATCH 03/13] add changelog and generalize --- CHANGELOG_UNRELEASED.md | 33 ++++++++ theories/charge.v | 163 ++++++++++++++++++++++++---------------- 2 files changed, 132 insertions(+), 64 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3c9ab8514..65779b3a4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -75,6 +75,37 @@ `ae_eq_mul2l`, `ae_eq_mul1l`, `ae_eq_abse` + +- in `charge.v` + + `charge_add` instance of `charge` + + `cpushforward` instance of `charge` + + `charge_of_finite_measure` instance of `charge` + + lemma `cscaleE` + + lemma `dominates_cscale` + + lemma `caddE` + + lemma `dominates_caddl` + + lemma `dominates_pushforward` + + lemma `cjordan_posE` + + lemma `jordan_posE` + + lemma `cjordan_negE` + + lemma `jordan_negE` + + lemma `Radon_Nikodym_sigma_finite_fin_num` + + lemma `Radon_NikodymE` + + lemma `Radon_Nikodym_fin_num` + + lemma `ae_eq_Radon_Nikodym_SigmaFinite` + + lemma `Radon_Nikodym_change_of_variables` + + lemma `Radon_Nikodym_cscale` + + lemma `Radon_Nikodym_cadd` + + lemma `Radon_Nikodym_chain_rule` + +### Changed + +- in `charge.v` + + definition `jordan_decomp` now uses `cadd` and `cscale` + + Definition `Radon_Nikodym_SigmaFinite` now be a module `Radon_Nikodym_SigmaFinite` with + * lemma `change_of_variables` + * lemma `integralM` + * lemma `chain_rule` ### Renamed @@ -85,6 +116,8 @@ - in `lebesgue_integral.v` + `ge0_integral_bigsetU` generalized from `nat` to `eqType` +- in `lebesgue_measure.v` + + an hypothesis of lemma `integral_ae_eq` is weakened ### Deprecated diff --git a/theories/charge.v b/theories/charge.v index ef660d002..f7403f3fc 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -35,6 +35,12 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* non-measurable sets *) (* czero == zero charge *) (* cscale r nu == charge nu scaled by a factor r : R *) +(* charge_add n1 n2 == the charge corresponding to the sum of *) +(* charges n1 and n2 *) +(* cpushforward nu mf == pushforward charge of nu along *) +(* measurable function f, mf is a proof that *) +(* f is measurable function *) +(* charge_of_finite_measure mu == charge corresponding to a finite measure mu *) (* *) (* * Theory *) (* nu.-positive_set P == P is a positive set with nu a charge *) @@ -400,14 +406,14 @@ Lemma dominates_cscale d (T : measurableType d) (R : realType) (mu : {sigma_finite_measure set T -> \bar R}) (nu : {charge set T -> \bar R}) (c : R) : nu `<< mu -> cscale c nu `<< mu. -Proof. by move=> numu E mE /numu; rewrite /cscale => ->//; rewrite mule0. Qed. +Proof. by move=> numu E mE /numu; rewrite cscaleE => ->//; rewrite mule0. Qed. Section charge_add. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). -Variables (m1 m2 : {charge set T -> \bar R}). +Variables (n1 n2 : {charge set T -> \bar R}). -Definition cadd := m1 \+ m2. +Definition cadd := n1 \+ n2. Let cadd0 : cadd set0 = 0. Proof. by rewrite /cadd 2!charge0 adde0. Qed. @@ -420,9 +426,9 @@ Proof. move=> F mF tF mUF; rewrite /cadd. under eq_fun do rewrite big_split; apply: cvg_trans. (* TODO: IIRC explicit arguments were added to please Coq 8.14, rm if not needed anymore *) - apply: (@cvgeD _ _ _ R (fun x => \sum_(0 <= i < x) (m1 (F i))) - (fun x => \sum_(0 <= i < x) (m2 (F i))) - (m1 (\bigcup_n F n)) (m2 (\bigcup_n F n))). + apply: (@cvgeD _ _ _ R (fun x => \sum_(0 <= i < x) (n1 (F i))) + (fun x => \sum_(0 <= i < x) (n2 (F i))) + (n1 (\bigcup_n F n)) (n2 (\bigcup_n F n))). - by rewrite fin_num_adde_defr// fin_num_measure. - exact: charge_semi_sigma_additive. - exact: charge_semi_sigma_additive. @@ -432,7 +438,7 @@ Qed. HB.instance Definition _ := isCharge.Build _ _ _ cadd cadd0 cadd_finite cadd_sigma_additive. -Lemma caddE E : cadd E = m1 E + m2 E. Proof. by []. Qed. +Lemma caddE E : cadd E = n1 E + n2 E. Proof. by []. Qed. End charge_add. @@ -442,7 +448,7 @@ Lemma dominates_caddl d (T : measurableType d) nu0 `<< mu -> nu1 `<< mu -> cadd nu0 nu1 `<< mu. Proof. -by move=> nu0mu nu1mu A mA A0; rewrite /cadd nu0mu// nu1mu// adde0. +by move=> nu0mu nu1mu A mA A0; rewrite caddE nu0mu// nu1mu// adde0. Qed. Section pushforward_charge. @@ -577,6 +583,74 @@ Qed. End positive_negative_set_realFieldType. + +Section min_cvg_0_cvg_0. +Context (R : realFieldType). + +Lemma minr_cvg_0_cvg_0 (x : R^nat) (p : R) : + (0 < p)%R -> (forall k, 0 <= x k)%R -> + (fun n => minr (x n) p)%R --> (0:R)%R -> x --> (0:R)%R. +Proof. +move=> p0 x_ge0 minr_cvg. +apply/(@cvgrPdist_lt _ [normedModType R of R^o]) => _ /posnumP[e]. +have : (0 < minr (e%:num) p)%R by rewrite lt_minr// p0 andbT. +move/(@cvgrPdist_lt _ [normedModType R of R^o]) : minr_cvg => /[apply] -[M _ hM]. +near=> n; rewrite sub0r normrN. +have /hM : (M <= n)%N by near: n; exists M. +rewrite sub0r normrN !ger0_norm// ?le_minr ?divr_ge0//=. + by move/lt_min_lt. +by rewrite x_ge0 ltW. +Unshelve. all: by end_near. Qed. + +Lemma mine_cvg_0_cvg_fin_num (x : (\bar R)^nat) (p : \bar R) : + (0 < p) -> (forall k, 0 <= x k) -> + (fun n => mine (x n) p) --> 0 -> + \forall n \near \oo, x n \is a fin_num. +Proof. +case : p => //; last first. +- move=> _ x_ge0. + under eq_cvg do rewrite miney. + by move/fine_cvgP => []. +- move=> p p0 x_ge0 /fine_cvgP[_]. + move=> /(@cvgrPdist_lt _ [normedModType R of R^o])/(_ _ p0)[N _ hN]. + near=> n; have /hN : (N <= n)%N by near: n; exists N. + rewrite sub0r normrN /= ger0_norm ?fine_ge0//; last first. + by rewrite le_minr x_ge0 ltW. + have := x_ge0 n; case: (x n) => //=; rewrite ltxx //=. +Unshelve. all: by end_near. Qed. + +Lemma mine_cvg_minr_cvg (x : (\bar R)^nat) (p : R) : + (0 < p)%R -> (forall k, 0 <= x k) -> + (fun n => mine (x n) p%:E) --> 0 -> + (fun n => minr ((fine \o x) n) p) --> (0:R)%R. +Proof. +move=> p0 x_ge0 mine_cvg. +apply: (cvg_trans _ (fine_cvg mine_cvg)). +move/fine_cvgP : mine_cvg => [_ /=] /(@cvgrPdist_lt _ [normedModType R of R^o]). +move=> /(_ _ p0)[N _ hN]; apply: near_eq_cvg; near=> n. +have xnoo : x n < +oo. + rewrite ltNge leye_eq; apply/eqP => xnoo. + have /hN : (N <= n)%N by near: n; exists N. + by rewrite /= sub0r normrN xnoo //= gtr0_norm // ltxx. +by rewrite /= -(@fineK _ (x n)) ?ge0_fin_numE//= -fine_min. +Unshelve. all: by end_near. Qed. + +Lemma mine_cvg_0_cvg_0 (x : (\bar R)^nat) (p : \bar R) : + (0 < p) -> (forall k, 0 <= x k) -> + (fun n => mine (x n) p) --> 0 -> x --> 0. +Proof. +move=> p0 x_ge0 h; apply/fine_cvgP; split; first exact: (mine_cvg_0_cvg_fin_num p0). +case: p p0 h => //; last first. +- move=> _. + under eq_cvg do rewrite miney. + exact: fine_cvg. +- move=> p p0 h. + apply: (@minr_cvg_0_cvg_0 (fine \o x) p) => //; last exact: mine_cvg_minr_cvg. + by move=> k /=; rewrite fine_ge0. +Qed. + +End min_cvg_0_cvg_0. + Section hahn_decomposition_lemma. Context d (T : measurableType d) (R : realType). Variables (nu : {charge set T -> \bar R}) (D : set T). @@ -624,55 +698,19 @@ have /ereal_sup_gt/cid2[_ [B/= [mB BDA <- mnuB]]] : m < d_ A. by exists B; split => //; rewrite (le_trans _ (ltW mnuB)). Qed. -(* TODO: generalize? *) -Let minr_cvg_0_cvg_0 (x : R^nat) : (forall k, 0 <= x k)%R -> - (fun n => minr (x n * 2^-1) 1)%R --> (0:R)%R -> x --> (0:R)%R. -Proof. -move=> x_ge0 minr_cvg. -apply/(@cvgrPdist_lt _ [normedModType R of R^o]) => _ /posnumP[e]. -have : (0 < minr (e%:num / 2) 1)%R by rewrite lt_minr// ltr01 andbT divr_gt0. -move/(@cvgrPdist_lt _ [normedModType R of R^o]) : minr_cvg => /[apply] -[M _ hM]. -near=> n; rewrite sub0r normrN. -have /hM : (M <= n)%N by near: n; exists M. -rewrite sub0r normrN !ger0_norm// ?le_minr ?divr_ge0//=. -rewrite -[X in minr _ X](@divrr _ 2) ?unitfE -?minr_pmull//. -rewrite -[X in (_ < minr _ X)%R](@divrr _ 2) ?unitfE -?minr_pmull//. -by rewrite ltr_pmul2r//; exact: lt_min_lt. -Unshelve. all: by end_near. Qed. - -Let mine_cvg_0_cvg_fin_num (x : (\bar R)^nat) : (forall k, 0 <= x k) -> - (fun n => mine (x n * (2^-1)%:E) 1) --> 0 -> - \forall n \near \oo, x n \is a fin_num. -Proof. -move=> x_ge0 /fine_cvgP[_]. -move=> /(@cvgrPdist_lt _ [normedModType R of R^o])/(_ _ ltr01)[N _ hN]. -near=> n; have /hN : (N <= n)%N by near: n; exists N. -rewrite sub0r normrN /= ger0_norm ?fine_ge0//; last first. - by rewrite le_minr mule_ge0//=. -by have := x_ge0 n; case: (x n) => //=; rewrite gt0_mulye//= ltxx. -Unshelve. all: by end_near. Qed. - -Let mine_cvg_minr_cvg (x : (\bar R)^nat) : (forall k, 0 <= x k) -> - (fun n => mine (x n * (2^-1)%:E) 1) --> 0 -> - (fun n => minr ((fine \o x) n / 2) 1%R) --> (0:R)%R. -Proof. -move=> x_ge0 mine_cvg. -apply: (cvg_trans _ (fine_cvg mine_cvg)). -move/fine_cvgP : mine_cvg => [_ /=] /(@cvgrPdist_lt _ [normedModType R of R^o]). -move=> /(_ _ ltr01)[N _ hN]; apply: near_eq_cvg; near=> n. -have xnoo : x n < +oo. - rewrite ltNge leye_eq; apply/eqP => xnoo. - have /hN : (N <= n)%N by near: n; exists N. - by rewrite /= sub0r normrN xnoo gt0_mulye//= normr1 ltxx. -by rewrite /= -(@fineK _ (x n)) ?ge0_fin_numE//= -fine_min. -Unshelve. all: by end_near. Qed. - -Let mine_cvg_0_cvg_0 (x : (\bar R)^nat) : (forall k, 0 <= x k) -> - (fun n => mine (x n * (2^-1)%:E) 1) --> 0 -> x --> 0. +Let mine2_cvg_0_cvg_0 (x : (\bar R)^nat) : + (forall k, 0 <= x k) -> + (fun n => mine (x n * 2^-1%:E) 1) --> 0 -> x --> 0. Proof. -move=> x_ge0 h; apply/fine_cvgP; split; first exact: mine_cvg_0_cvg_fin_num. -apply: (@minr_cvg_0_cvg_0 (fine \o x)) => //; last exact: mine_cvg_minr_cvg. -by move=> k /=; rewrite fine_ge0. +move=> x_ge0 h. +have x2x2 : x =1 (fun n => 2%:E * (x n * 2^-1%:E)). + move=> n. + by rewrite muleCA -EFinM divff ?mule1. +under eq_cvg do rewrite x2x2. +rewrite -(mule0 2%:E). +apply: cvgeMl => //. +apply: (mine_cvg_0_cvg_0 lte01) => //. +by move=> n; rewrite mule_ge0. Qed. Lemma hahn_decomposition_lemma : measurable D -> @@ -717,7 +755,7 @@ have mine_cvg_0 : (fun n => mine (g_ (v n) * 2^-1%:E) 1) --> 0. apply: (@squeeze_cvge _ _ _ _ _ _ (fun n => nu (A_ (v n)))); [|exact: cvg_cst|by []]. by apply: nearW => n /=; rewrite nuA_g_ andbT le_minr lee01 andbT mule_ge0. -have d_cvg_0 : g_ \o v --> 0 by apply: mine_cvg_0_cvg_0 => //=. +have d_cvg_0 : g_ \o v --> 0 by apply: mine2_cvg_0_cvg_0 => //=. have nuDAoo : nu D >= nu (D `\` Aoo). rewrite -[in leRHS](@setDUK _ Aoo D); last first. by apply: bigcup_sub => i _; exact: A_D. @@ -1545,21 +1583,18 @@ Qed. End radon_nikodym_finite. -(* TODO: move? *) +(* PR:#1110 *) Lemma measure_dominates_ae_eq d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (nu : {measure set T -> \bar R}) (f g : T -> \bar R) E : measurable E -> nu `<< mu -> ae_eq mu E f g -> ae_eq nu E f g. -Proof. by move=> mE munu [A [mA A0 EA]]; exists A; split => //; exact: munu. Qed. +Proof. Admitted. -(* TODO: move *) +(* PR:#1110 *) Lemma ae_eqS d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) A B f g : B `<=` A -> ae_eq mu A f g -> ae_eq mu B f g. Proof. -move=> BA. -case => N [mN N0 fg]; exists N; split => //. -by apply: subset_trans fg; apply: subsetC => z /= /[swap] /BA ? ->//. -Qed. +Admitted. Section radon_nikodym_sigma_finite. Context d (T : measurableType d) (R : realType). From 47aa95455b57ae4d5095ed4234f7b073ee717ffd Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Mon, 11 Dec 2023 16:08:58 +0900 Subject: [PATCH 04/13] add max_cvg_0_cvg_0 --- CHANGELOG_UNRELEASED.md | 9 +++++ theories/charge.v | 78 ++++++++++++++++++++++++++++++++++++++++- 2 files changed, 86 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 65779b3a4..f77f4dc42 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -98,6 +98,15 @@ + lemma `Radon_Nikodym_cadd` + lemma `Radon_Nikodym_chain_rule` + + lemma `minr_cvg_0_cvg_0` + + lemma `mine_cvg_0_cvg_fin_num` + + lemma `mine_cvg_minr_cvg` + + lemma `mine_cvg_0_cvg_0` + + lemma `maxr_cvg_0_cvg_0` + + lemma `maxe_cvg_0_cvg_fin_num` + + lemma `maxe_cvg_maxr_cvg` + + lemma `maxe_cvg_0_cvg_0` + ### Changed - in `charge.v` diff --git a/theories/charge.v b/theories/charge.v index f7403f3fc..29fc22448 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -583,7 +583,7 @@ Qed. End positive_negative_set_realFieldType. - +(* TODO: generalize *) Section min_cvg_0_cvg_0. Context (R : realFieldType). @@ -651,6 +651,82 @@ Qed. End min_cvg_0_cvg_0. +Section max_cvg_0_cvg_0. +Context (R : realFieldType). + +Lemma maxr_cvg_0_cvg_0 (x : R^nat) (np : R) : + (np < 0)%R -> (forall k, x k <= 0)%R -> + (fun n => maxr (x n) np)%R --> (0:R)%R -> x --> (0:R)%R. +Proof. +move=> np0 x_le0. +under eq_fun do rewrite -(opprK (x _)) -{1}(opprK np) -oppr_min. +rewrite -oppr0. +move/(@cvgNP _ [normedModType R of R^o]). +move/minr_cvg_0_cvg_0. +rewrite -oppr0 ltr_oppr in np0. +move/(_ np0). +have oppx_ge0 : (forall k : nat, (0 <= - x k)%R); first by move=> n; rewrite ler_oppr oppr0. +move/(_ oppx_ge0). +move/(@cvgNP _ [normedModType R of R^o]). +by rewrite opprK. +Qed. + +Lemma maxe_cvg_0_cvg_fin_num (x : (\bar R)^nat) (np : \bar R) : + (np < 0) -> (forall k, x k <= 0) -> + (fun n => maxe (x n) np) --> 0 -> + \forall n \near \oo, x n \is a fin_num. +Proof. +move=> np0 x_le0. +under eq_fun do rewrite -(oppeK (x _)) -{1}(oppeK np) -oppe_min. +rewrite -oppe0. +move/cvgeNP. +move/mine_cvg_0_cvg_fin_num. +rewrite -oppe0 lte_oppr in np0. +move/(_ np0). +have oppx_ge0 : (forall k : nat, 0 <= - x k); first by move=> n; rewrite lee_oppr oppe0. +move/(_ oppx_ge0). +move=> [] n _ Hn. +exists n => // k nk. +rewrite -fin_numN. +by apply: Hn. +Qed. + +Lemma maxe_cvg_maxr_cvg (x : (\bar R)^nat) (np : R) : + (np < 0)%R -> (forall k, x k <= 0) -> + (fun n => maxe (x n) np%:E) --> 0 -> + (fun n => maxr ((fine \o x) n) np) --> (0:R)%R. +Proof. +move=> np0 x_le0. +under eq_fun do rewrite -(oppeK (x _)) -{1}(oppeK np%:E) -oppe_min. +rewrite -oppr0 EFinN. +move/cvgeNP. +move/mine_cvg_minr_cvg. +rewrite -oppr0 ltr_oppr in np0. +move/(_ np0). +have oppx_ge0 : (forall k : nat, 0 <= - x k); first by move=> n; rewrite lee_oppr oppe0. +move/(_ oppx_ge0). +move/(@cvgNP _ [normedModType R of R^o]). +by under eq_cvg do rewrite /GRing.opp /= oppr_min fineN !opprK. +Qed. + +Lemma maxe_cvg_0_cvg_0 (x : (\bar R)^nat) (np : \bar R) : + (np < 0) -> (forall k, x k <= 0) -> + (fun n => maxe (x n) np) --> 0 -> x --> 0. +Proof. +move=> np0 x_le0. +under eq_fun do rewrite -(oppeK (x _)) -{1}(oppeK np) -oppe_min. +rewrite -oppe0. +move/cvgeNP. +move/mine_cvg_0_cvg_0. +rewrite -oppe0 lte_oppr in np0. +move/(_ np0). +have oppx_ge0 : (forall k : nat, 0 <= - x k); first by move=> n; rewrite lee_oppr oppe0. +move/(_ oppx_ge0) /cvgeNP. +by under eq_cvg do rewrite oppeK. +Qed. + +End max_cvg_0_cvg_0. + Section hahn_decomposition_lemma. Context d (T : measurableType d) (R : realType). Variables (nu : {charge set T -> \bar R}) (D : set T). From 5881fe1c6b09f9f051be4c2e16a9b88b127e422a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 21 Dec 2023 16:12:44 +0900 Subject: [PATCH 05/13] fix --- CHANGELOG_UNRELEASED.md | 1 + theories/charge.v | 191 ++++------------------------------------ theories/measure.v | 8 +- theories/sequences.v | 125 ++++++++++++++++++++++++++ 4 files changed, 148 insertions(+), 177 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f77f4dc42..e5506238e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -98,6 +98,7 @@ + lemma `Radon_Nikodym_cadd` + lemma `Radon_Nikodym_chain_rule` +- in `sequences.v`: + lemma `minr_cvg_0_cvg_0` + lemma `mine_cvg_0_cvg_fin_num` + lemma `mine_cvg_minr_cvg` diff --git a/theories/charge.v b/theories/charge.v index 29fc22448..db081ab07 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -238,7 +238,7 @@ Local Notation nu := (charge_of_finite_measure mu). Let nu0 : nu set0 = 0. Proof. exact: measure0. Qed. Let nu_finite S : measurable S -> nu S \is a fin_num. -Proof. by apply: fin_num_measure. Qed. +Proof. exact: fin_num_measure. Qed. Let nu_sigma_additive : semi_sigma_additive nu. Proof. exact: measure_semi_sigma_additive. Qed. @@ -442,8 +442,8 @@ Lemma caddE E : cadd E = n1 E + n2 E. Proof. by []. Qed. End charge_add. -Lemma dominates_caddl d (T : measurableType d) - (R : realType) (mu : {sigma_finite_measure set T -> \bar R}) +Lemma dominates_caddl d (T : measurableType d) (R : realType) + (mu : {sigma_finite_measure set T -> \bar R}) (nu0 nu1 : {charge set T -> \bar R}) : nu0 `<< mu -> nu1 `<< mu -> cadd nu0 nu1 `<< mu. @@ -453,7 +453,7 @@ Qed. Section pushforward_charge. Local Open Scope ereal_scope. -Context d d' (T1 : measurableType d) (T2 : measurableType d') (f : T1 -> T2). +Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (f : T1 -> T2). Variables (R : realFieldType) (nu : {charge set T1 -> \bar R}). Definition cpushforward (mf : measurable_fun setT f) A := nu (f @^-1` A). @@ -466,7 +466,7 @@ Proof. by rewrite /cpushforward preimage_set0 charge0. Qed. Let cpushforward_finite A : measurable A -> cpushforward mf A \is a fin_num. Proof. move=> mA; apply: fin_num_measure. -by rewrite -[X in measurable X]setTI; apply: mf. +by rewrite -[X in measurable X]setTI; exact: mf. Qed. Let cpushforward_sigma_additive : semi_sigma_additive (cpushforward mf). @@ -479,8 +479,8 @@ apply: charge_semi_sigma_additive. - by rewrite -preimage_bigcup -[X in measurable X]setTI; exact: mf. Qed. -HB.instance Definition _ := isCharge.Build _ _ _ - (cpushforward mf) cpushforward0 cpushforward_finite cpushforward_sigma_additive. +HB.instance Definition _ := isCharge.Build _ _ _ (cpushforward mf) + cpushforward0 cpushforward_finite cpushforward_sigma_additive. End pushforward_charge. @@ -521,6 +521,7 @@ End positive_negative_set. Notation "nu .-negative_set" := (negative_set nu) : charge_scope. Notation "nu .-positive_set" := (positive_set nu) : charge_scope. + Local Open Scope charge_scope. Section positive_negative_set_lemmas. @@ -583,150 +584,6 @@ Qed. End positive_negative_set_realFieldType. -(* TODO: generalize *) -Section min_cvg_0_cvg_0. -Context (R : realFieldType). - -Lemma minr_cvg_0_cvg_0 (x : R^nat) (p : R) : - (0 < p)%R -> (forall k, 0 <= x k)%R -> - (fun n => minr (x n) p)%R --> (0:R)%R -> x --> (0:R)%R. -Proof. -move=> p0 x_ge0 minr_cvg. -apply/(@cvgrPdist_lt _ [normedModType R of R^o]) => _ /posnumP[e]. -have : (0 < minr (e%:num) p)%R by rewrite lt_minr// p0 andbT. -move/(@cvgrPdist_lt _ [normedModType R of R^o]) : minr_cvg => /[apply] -[M _ hM]. -near=> n; rewrite sub0r normrN. -have /hM : (M <= n)%N by near: n; exists M. -rewrite sub0r normrN !ger0_norm// ?le_minr ?divr_ge0//=. - by move/lt_min_lt. -by rewrite x_ge0 ltW. -Unshelve. all: by end_near. Qed. - -Lemma mine_cvg_0_cvg_fin_num (x : (\bar R)^nat) (p : \bar R) : - (0 < p) -> (forall k, 0 <= x k) -> - (fun n => mine (x n) p) --> 0 -> - \forall n \near \oo, x n \is a fin_num. -Proof. -case : p => //; last first. -- move=> _ x_ge0. - under eq_cvg do rewrite miney. - by move/fine_cvgP => []. -- move=> p p0 x_ge0 /fine_cvgP[_]. - move=> /(@cvgrPdist_lt _ [normedModType R of R^o])/(_ _ p0)[N _ hN]. - near=> n; have /hN : (N <= n)%N by near: n; exists N. - rewrite sub0r normrN /= ger0_norm ?fine_ge0//; last first. - by rewrite le_minr x_ge0 ltW. - have := x_ge0 n; case: (x n) => //=; rewrite ltxx //=. -Unshelve. all: by end_near. Qed. - -Lemma mine_cvg_minr_cvg (x : (\bar R)^nat) (p : R) : - (0 < p)%R -> (forall k, 0 <= x k) -> - (fun n => mine (x n) p%:E) --> 0 -> - (fun n => minr ((fine \o x) n) p) --> (0:R)%R. -Proof. -move=> p0 x_ge0 mine_cvg. -apply: (cvg_trans _ (fine_cvg mine_cvg)). -move/fine_cvgP : mine_cvg => [_ /=] /(@cvgrPdist_lt _ [normedModType R of R^o]). -move=> /(_ _ p0)[N _ hN]; apply: near_eq_cvg; near=> n. -have xnoo : x n < +oo. - rewrite ltNge leye_eq; apply/eqP => xnoo. - have /hN : (N <= n)%N by near: n; exists N. - by rewrite /= sub0r normrN xnoo //= gtr0_norm // ltxx. -by rewrite /= -(@fineK _ (x n)) ?ge0_fin_numE//= -fine_min. -Unshelve. all: by end_near. Qed. - -Lemma mine_cvg_0_cvg_0 (x : (\bar R)^nat) (p : \bar R) : - (0 < p) -> (forall k, 0 <= x k) -> - (fun n => mine (x n) p) --> 0 -> x --> 0. -Proof. -move=> p0 x_ge0 h; apply/fine_cvgP; split; first exact: (mine_cvg_0_cvg_fin_num p0). -case: p p0 h => //; last first. -- move=> _. - under eq_cvg do rewrite miney. - exact: fine_cvg. -- move=> p p0 h. - apply: (@minr_cvg_0_cvg_0 (fine \o x) p) => //; last exact: mine_cvg_minr_cvg. - by move=> k /=; rewrite fine_ge0. -Qed. - -End min_cvg_0_cvg_0. - -Section max_cvg_0_cvg_0. -Context (R : realFieldType). - -Lemma maxr_cvg_0_cvg_0 (x : R^nat) (np : R) : - (np < 0)%R -> (forall k, x k <= 0)%R -> - (fun n => maxr (x n) np)%R --> (0:R)%R -> x --> (0:R)%R. -Proof. -move=> np0 x_le0. -under eq_fun do rewrite -(opprK (x _)) -{1}(opprK np) -oppr_min. -rewrite -oppr0. -move/(@cvgNP _ [normedModType R of R^o]). -move/minr_cvg_0_cvg_0. -rewrite -oppr0 ltr_oppr in np0. -move/(_ np0). -have oppx_ge0 : (forall k : nat, (0 <= - x k)%R); first by move=> n; rewrite ler_oppr oppr0. -move/(_ oppx_ge0). -move/(@cvgNP _ [normedModType R of R^o]). -by rewrite opprK. -Qed. - -Lemma maxe_cvg_0_cvg_fin_num (x : (\bar R)^nat) (np : \bar R) : - (np < 0) -> (forall k, x k <= 0) -> - (fun n => maxe (x n) np) --> 0 -> - \forall n \near \oo, x n \is a fin_num. -Proof. -move=> np0 x_le0. -under eq_fun do rewrite -(oppeK (x _)) -{1}(oppeK np) -oppe_min. -rewrite -oppe0. -move/cvgeNP. -move/mine_cvg_0_cvg_fin_num. -rewrite -oppe0 lte_oppr in np0. -move/(_ np0). -have oppx_ge0 : (forall k : nat, 0 <= - x k); first by move=> n; rewrite lee_oppr oppe0. -move/(_ oppx_ge0). -move=> [] n _ Hn. -exists n => // k nk. -rewrite -fin_numN. -by apply: Hn. -Qed. - -Lemma maxe_cvg_maxr_cvg (x : (\bar R)^nat) (np : R) : - (np < 0)%R -> (forall k, x k <= 0) -> - (fun n => maxe (x n) np%:E) --> 0 -> - (fun n => maxr ((fine \o x) n) np) --> (0:R)%R. -Proof. -move=> np0 x_le0. -under eq_fun do rewrite -(oppeK (x _)) -{1}(oppeK np%:E) -oppe_min. -rewrite -oppr0 EFinN. -move/cvgeNP. -move/mine_cvg_minr_cvg. -rewrite -oppr0 ltr_oppr in np0. -move/(_ np0). -have oppx_ge0 : (forall k : nat, 0 <= - x k); first by move=> n; rewrite lee_oppr oppe0. -move/(_ oppx_ge0). -move/(@cvgNP _ [normedModType R of R^o]). -by under eq_cvg do rewrite /GRing.opp /= oppr_min fineN !opprK. -Qed. - -Lemma maxe_cvg_0_cvg_0 (x : (\bar R)^nat) (np : \bar R) : - (np < 0) -> (forall k, x k <= 0) -> - (fun n => maxe (x n) np) --> 0 -> x --> 0. -Proof. -move=> np0 x_le0. -under eq_fun do rewrite -(oppeK (x _)) -{1}(oppeK np) -oppe_min. -rewrite -oppe0. -move/cvgeNP. -move/mine_cvg_0_cvg_0. -rewrite -oppe0 lte_oppr in np0. -move/(_ np0). -have oppx_ge0 : (forall k : nat, 0 <= - x k); first by move=> n; rewrite lee_oppr oppe0. -move/(_ oppx_ge0) /cvgeNP. -by under eq_cvg do rewrite oppeK. -Qed. - -End max_cvg_0_cvg_0. - Section hahn_decomposition_lemma. Context d (T : measurableType d) (R : realType). Variables (nu : {charge set T -> \bar R}) (D : set T). @@ -774,15 +631,13 @@ have /ereal_sup_gt/cid2[_ [B/= [mB BDA <- mnuB]]] : m < d_ A. by exists B; split => //; rewrite (le_trans _ (ltW mnuB)). Qed. -Let mine2_cvg_0_cvg_0 (x : (\bar R)^nat) : - (forall k, 0 <= x k) -> - (fun n => mine (x n * 2^-1%:E) 1) --> 0 -> x --> 0. +Let mine2_cvg_0_cvg_0 (u : (\bar R)^nat) : (forall k, 0 <= u k) -> + mine (u n * 2^-1%:E) 1 @[n --> \oo] --> 0 -> u --> 0. Proof. -move=> x_ge0 h. -have x2x2 : x =1 (fun n => 2%:E * (x n * 2^-1%:E)). - move=> n. - by rewrite muleCA -EFinM divff ?mule1. -under eq_cvg do rewrite x2x2. +move=> u0 h. +have u2u2 : u =1 (fun n => 2%:E * (u n * 2^-1%:E)). + by move=> n; rewrite muleCA -EFinM divff ?mule1. +under eq_cvg do rewrite u2u2. rewrite -(mule0 2%:E). apply: cvgeMl => //. apply: (mine_cvg_0_cvg_0 lte01) => //. @@ -1035,7 +890,8 @@ Let mP : measurable P. Proof. by have [[mP _] _ _ _] := nuPN. Qed. Let mN : measurable N. Proof. by have [_ [mN _] _ _] := nuPN. Qed. -Local Definition cjordan_pos : {charge set T -> \bar R} := [the charge _ _ of crestr0 nu mP]. +Local Definition cjordan_pos : {charge set T -> \bar R} := + [the charge _ _ of crestr0 nu mP]. Lemma cjordan_posE A : cjordan_pos A = crestr0 nu mP A. Proof. by []. Qed. @@ -1659,19 +1515,6 @@ Qed. End radon_nikodym_finite. -(* PR:#1110 *) -Lemma measure_dominates_ae_eq d (T : measurableType d) (R : realType) - (mu : {measure set T -> \bar R}) (nu : {measure set T -> \bar R}) - (f g : T -> \bar R) E : measurable E -> - nu `<< mu -> ae_eq mu E f g -> ae_eq nu E f g. -Proof. Admitted. - -(* PR:#1110 *) -Lemma ae_eqS d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) A B f g : - B `<=` A -> ae_eq mu A f g -> ae_eq mu B f g. -Proof. -Admitted. - Section radon_nikodym_sigma_finite. Context d (T : measurableType d) (R : realType). Variables (mu : {sigma_finite_measure set T -> \bar R}) @@ -1791,7 +1634,7 @@ exists g; split => //. - move=> A mA; rewrite nuf ?inE//; apply: ae_eq_integral => //. + exact: measurable_funTS. + exact: measurable_funTS. - + exact: ae_eqS fg. + + exact: ae_eq_subset fg. Qed. End radon_nikodym_sigma_finite. diff --git a/theories/measure.v b/theories/measure.v index ec7f86fae..d8a0cdb4d 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4498,6 +4498,11 @@ Implicit Types m : set T -> \bar R. Definition measure_dominates m1 m2 := forall A, measurable A -> m2 A = 0 -> m1 A = 0. +Local Notation "m1 `<< m2" := (measure_dominates m1 m2). + +Lemma measure_dominates_trans m1 m2 m3 : m1 `<< m2 -> m2 `<< m3 -> m1 `<< m3. +Proof. by move=> m12 m23 A mA /m23-/(_ mA) /m12; exact. Qed. + End absolute_continuity. Notation "m1 `<< m2" := (measure_dominates m1 m2). @@ -4505,9 +4510,6 @@ Section absolute_continuity_lemmas. Context d (T : measurableType d) (R : realType). Implicit Types m : {measure set T -> \bar R}. -Lemma measure_dominates_trans m1 m2 m3 : m1 `<< m2 -> m2 `<< m3 -> m1 `<< m3. -Proof. by move=> m12 m23 A mA /m23-/(_ mA) /m12; exact. Qed. - Lemma measure_dominates_ae_eq m1 m2 f g E : measurable E -> m2 `<< m1 -> ae_eq m1 E f g -> ae_eq m2 E f g. Proof. by move=> mE m21 [A [mA A0 ?]]; exists A; split => //; exact: m21. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index 3ab4bc475..c5803f14d 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -2052,6 +2052,131 @@ Notation nneseries_pred0 := eseries_pred0 (only parsing). #[deprecated(since="analysis 0.6.0", note="Use eseries_mkcond instead.")] Notation nneseries_mkcond := eseries_mkcond (only parsing). +Section minr_cvg_0. +Local Open Scope ring_scope. +Context {R : realFieldType}. +Implicit Types (u : R^nat) (r : R). + +Lemma minr_cvg_0_cvg_0 u r : 0 < r -> (forall k, 0 <= u k) -> + minr (u n) r @[n --> \oo] --> (0:R) -> u --> (0:R). +Proof. +move=> r0 u0 minr_cvg; apply/cvgrPdist_lt => _ /posnumP[e]. +have : 0 < minr e%:num r by rewrite lt_minr// r0 andbT. +move/cvgrPdist_lt : minr_cvg => /[apply] -[M _ hM]. +near=> n; rewrite sub0r normrN. +have /hM : (M <= n)%N by near: n; exists M. +rewrite sub0r normrN (ger0_norm (u0 n)) ger0_norm//; last first. + by rewrite le_minr u0 ltW. +by move/lt_min_lt. +Unshelve. all: by end_near. Qed. + +Lemma maxr_cvg_0_cvg_0 u r : r < 0 -> (forall k, u k <= 0) -> + maxr (u n) r @[n --> \oo] --> (0:R) -> u --> (0:R). +Proof. +move=> r0 u0. +under eq_fun do rewrite -(opprK (u _)) -{1}(opprK r) -oppr_min. +rewrite -oppr0. +move/cvgNP/minr_cvg_0_cvg_0. +rewrite -oppr0 ltr_oppr in r0. +move/(_ r0). +have Nu0 k : 0 <= - u k by rewrite ler_oppr oppr0. +by move=> /(_ Nu0)/cvgNP; rewrite opprK. +Qed. + +End minr_cvg_0. + +Section mine_cvg_0. +Context {R : realFieldType}. +Local Open Scope ereal_scope. +Implicit Types (u : (\bar R)^nat) (r : R) (x : \bar R). + +Lemma mine_cvg_0_cvg_fin_num u x : 0 < x -> (forall k, 0 <= u k) -> + mine (u n) x @[n --> \oo] --> 0 -> + \forall n \near \oo, u n \is a fin_num. +Proof. +case: x => [r r0 u0 /fine_cvgP[_]|_ u0|//]; last first. + under eq_cvg do rewrite miney. + by case/fine_cvgP. +move=> /cvgrPdist_lt/(_ _ r0)[N _ hN]. +near=> n; have /hN : (N <= n)%N by near: n; exists N. +rewrite sub0r normrN /= ger0_norm ?fine_ge0//; last first. + by rewrite le_minr u0 ltW. +by have := u0 n; case: (u n) => //=; rewrite ltxx. +Unshelve. all: by end_near. Qed. + +Lemma mine_cvg_minr_cvg u r : (0 < r)%R -> (forall k, 0 <= u k) -> + mine (u n) r%:E @[n --> \oo] --> 0 -> + minr (fine (u n)) r @[n --> \oo] --> (0:R)%R. +Proof. +move=> r0 u0 mine_cvg; apply: (cvg_trans _ (fine_cvg mine_cvg)). +move/fine_cvgP : mine_cvg => [_ /=] /cvgrPdist_lt. +move=> /(_ _ r0)[N _ hN]; apply: near_eq_cvg; near=> n. +have xnoo : u n < +oo. + rewrite ltNge leye_eq; apply/eqP => xnoo. + have /hN : (N <= n)%N by near: n; exists N. + by rewrite /= sub0r normrN xnoo //= gtr0_norm // ltxx. +by rewrite /= -(@fineK _ (u n)) ?ge0_fin_numE//= -fine_min. +Unshelve. all: by end_near. Qed. + +Lemma mine_cvg_0_cvg_0 u x : 0 < x -> (forall k, 0 <= u k) -> + mine (u n) x @[n --> \oo] --> 0 -> u --> 0. +Proof. +move=> x0 u0 h; apply/fine_cvgP; split. + exact: (mine_cvg_0_cvg_fin_num x0). +case: x x0 h => [r r0 h|_|//]; last first. + under eq_cvg do rewrite miney. + exact: fine_cvg. +apply: (@minr_cvg_0_cvg_0 _ (fine \o u) r) => //. + by move=> k /=; rewrite fine_ge0. +exact: mine_cvg_minr_cvg. +Qed. + +Lemma maxe_cvg_0_cvg_fin_num u x : x < 0 -> (forall k, u k <= 0) -> + maxe (u n) x @[n --> \oo] --> 0 -> + \forall n \near \oo, u n \is a fin_num. +Proof. +move=> x0 u0. +under eq_fun do rewrite -(oppeK (u _)) -{1}(oppeK x) -oppe_min. +rewrite -oppe0. +move/cvgeNP/mine_cvg_0_cvg_fin_num. +rewrite -oppe0 lte_oppr in x0. +move/(_ x0). +have Nu0 k : 0 <= - u k by rewrite lee_oppr oppe0. +move=> /(_ Nu0)[n _ Hn]. +by exists n => // k nk; rewrite -fin_numN; exact: Hn. +Qed. + +Lemma maxe_cvg_maxr_cvg u r : (r < 0)%R -> (forall k, u k <= 0) -> + maxe (u n) r%:E @[n --> \oo] --> 0 -> + maxr (fine (u n)) r @[n --> \oo] --> (0:R)%R. +Proof. +move=> r0 u0. +under eq_fun do rewrite -(oppeK (u _)) -{1}(oppeK r%:E) -oppe_min. +rewrite -oppr0 EFinN. +move/cvgeNP/mine_cvg_minr_cvg. +rewrite -oppr0 ltr_oppr in r0. +move/(_ r0). +have Nu0 k : 0 <= - u k by rewrite lee_oppr oppe0. +move=> /(_ Nu0)/cvgNP. +by under eq_cvg do rewrite /GRing.opp /= oppr_min fineN !opprK. +Qed. + +Lemma maxe_cvg_0_cvg_0 u x : x < 0 -> (forall k, u k <= 0) -> + maxe (u n) x @[n --> \oo] --> 0 -> u --> 0. +Proof. +move=> x0 u0. +under eq_fun do rewrite -(oppeK (u _)) -{1}(oppeK x) -oppe_min. +rewrite -oppe0. +move/cvgeNP/mine_cvg_0_cvg_0. +rewrite -oppe0 lte_oppr in x0. +move/(_ x0). +have Nu0 k : 0 <= - u k by rewrite lee_oppr oppe0. +move=> /(_ Nu0)/cvgeNP. +by under eq_cvg do rewrite oppeK. +Qed. + +End mine_cvg_0. + Definition sdrop T (u : T^nat) n := [set u k | k in [set k | k >= n]]%N. Section sdrop. From 444560a52a167545d944b2de76f5d665314c890d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 26 Dec 2023 19:00:02 +0900 Subject: [PATCH 06/13] addressing comments by Quentin (wip) Co-authored-by: Tragicus <96025499+Tragicus@users.noreply.github.com> --- CHANGELOG_UNRELEASED.md | 54 ++++---- theories/charge.v | 236 +++++++++++++++-------------------- theories/lebesgue_integral.v | 3 +- theories/sequences.v | 51 +++----- 4 files changed, 147 insertions(+), 197 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e5506238e..f07addd8a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,42 +56,26 @@ - in file `measure.v` + add lemmas `ae_eq_subset`, `measure_dominates_ae_eq`. -### Changed - -- in `normedtype.v`: - + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns - duplicate-free lists of indices - -- moved from `lebesgue_integral.v` to `measure.v`: - + definition `ae_eq` - + lemmas - `ae_eq0`, - `ae_eq_comp`, - `ae_eq_funeposneg`, - `ae_eq_refl`, - `ae_eq_trans`, - `ae_eq_sub`, - `ae_eq_mul2r`, - `ae_eq_mul2l`, - `ae_eq_mul1l`, - `ae_eq_abse` - - in `charge.v` - + `charge_add` instance of `charge` - + `cpushforward` instance of `charge` - + `charge_of_finite_measure` instance of `charge` + + definition `charge_of_finite_measure` (instance of `charge`) + lemma `cscaleE` + lemma `dominates_cscale` + lemma `caddE` - + lemma `dominates_caddl` + + definition `cpushforward` (instance of `charge`) + lemma `dominates_pushforward` + lemma `cjordan_posE` + lemma `jordan_posE` + lemma `cjordan_negE` + lemma `jordan_negE` + lemma `Radon_Nikodym_sigma_finite_fin_num` - + lemma `Radon_NikodymE` + + module `Radon_Nikodym_SigmaFinite` + * definition `f` + * lemmas `f_ge0`, `f_fin_num`, `f_integrable`, `f_integral` + * lemma `change_of_variables` + * lemma `integrableM` + * lemma `chain_rule` + lemma `Radon_Nikodym_fin_num` + + lemma `Radon_Nikodym_integral` + lemma `ae_eq_Radon_Nikodym_SigmaFinite` + lemma `Radon_Nikodym_change_of_variables` + lemma `Radon_Nikodym_cscale` @@ -110,6 +94,24 @@ ### Changed +- in `normedtype.v`: + + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns + duplicate-free lists of indices + +- moved from `lebesgue_integral.v` to `measure.v`: + + definition `ae_eq` + + lemmas + `ae_eq0`, + `ae_eq_comp`, + `ae_eq_funeposneg`, + `ae_eq_refl`, + `ae_eq_trans`, + `ae_eq_sub`, + `ae_eq_mul2r`, + `ae_eq_mul2l`, + `ae_eq_mul1l`, + `ae_eq_abse` + - in `charge.v` + definition `jordan_decomp` now uses `cadd` and `cscale` + Definition `Radon_Nikodym_SigmaFinite` now be a module `Radon_Nikodym_SigmaFinite` with @@ -121,6 +123,8 @@ - in `exp.v`: + `lnX` -> `lnXn` +- in `charge.v`: + + `dominates_caddl` -> `dominates_cadd` ### Generalized diff --git a/theories/charge.v b/theories/charge.v index db081ab07..39c9f0905 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -137,7 +137,6 @@ HB.instance Definition _ := HB.end. Section charge_lemmas. - Context d (T : ringOfSetsType d) (R : numFieldType). Implicit Type nu : {charge set T -> \bar R}. @@ -226,14 +225,13 @@ HB.instance Definition _ := isMeasure.Build _ T R (measure_of_charge nupos) End measure_of_charge. Arguments measure_of_charge {d T R}. -Definition charge_of_finite_measure d (T : measurableType d) (R : realType) - (mu : {finite_measure set T -> \bar R}) : set T -> \bar R := mu. - Section charge_of_finite_measure. Context d (T : measurableType d) (R : realType). Variables (mu : {finite_measure set T -> \bar R}). -Local Notation nu := (charge_of_finite_measure mu). +Definition charge_of_finite_measure : set T -> \bar R := mu. + +Local Notation nu := charge_of_finite_measure. Let nu0 : nu set0 = 0. Proof. exact: measure0. Qed. @@ -243,7 +241,7 @@ Proof. exact: fin_num_measure. Qed. Let nu_sigma_additive : semi_sigma_additive nu. Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ := isCharge.Build _ T R (charge_of_finite_measure mu) +HB.instance Definition _ := isCharge.Build _ T R nu nu0 nu_finite nu_sigma_additive. End charge_of_finite_measure. @@ -403,7 +401,7 @@ Lemma cscaleE A : cscale A = r%:E * nu A. Proof. by []. Qed. End charge_scale. Lemma dominates_cscale d (T : measurableType d) (R : realType) - (mu : {sigma_finite_measure set T -> \bar R}) + (mu : set T -> \bar R) (nu : {charge set T -> \bar R}) (c : R) : nu `<< mu -> cscale c nu `<< mu. Proof. by move=> numu E mE /numu; rewrite cscaleE => ->//; rewrite mule0. Qed. @@ -442,7 +440,7 @@ Lemma caddE E : cadd E = n1 E + n2 E. Proof. by []. Qed. End charge_add. -Lemma dominates_caddl d (T : measurableType d) (R : realType) +Lemma dominates_cadd d (T : measurableType d) (R : realType) (mu : {sigma_finite_measure set T -> \bar R}) (nu0 nu1 : {charge set T -> \bar R}) : nu0 `<< mu -> nu1 `<< mu -> @@ -491,14 +489,15 @@ Let mu0 : mu set0 = 0. Proof. by apply: measure0. Qed. HB.instance Definition _ := isCharge.Build _ _ _ - mu (measure0 [the content _ _ of mu]) fin_num_measure measure_semi_sigma_additive. + mu (measure0 [the content _ _ of mu]) + fin_num_measure measure_semi_sigma_additive. HB.end. Section dominates_pushforward. Lemma dominates_pushforward d d' (T : measurableType d) (T' : measurableType d') - (R : realType) (mu : {sigma_finite_measure set T -> \bar R}) + (R : realType) (mu : {measure set T -> \bar R}) (nu : {charge set T -> \bar R}) (f : T -> T') (mf : measurable_fun setT f) : nu `<< mu -> cpushforward nu mf `<< pushforward mu mf. Proof. @@ -635,13 +634,10 @@ Let mine2_cvg_0_cvg_0 (u : (\bar R)^nat) : (forall k, 0 <= u k) -> mine (u n * 2^-1%:E) 1 @[n --> \oo] --> 0 -> u --> 0. Proof. move=> u0 h. -have u2u2 : u =1 (fun n => 2%:E * (u n * 2^-1%:E)). - by move=> n; rewrite muleCA -EFinM divff ?mule1. -under eq_cvg do rewrite u2u2. -rewrite -(mule0 2%:E). -apply: cvgeMl => //. -apply: (mine_cvg_0_cvg_0 lte01) => //. -by move=> n; rewrite mule_ge0. +have u2 n : u n = 2%:E * (u n * 2^-1%:E) by rewrite muleCA -EFinM divff ?mule1. +under eq_cvg do rewrite u2. +rewrite -(mule0 2%:E); apply: cvgeMl => //. +by apply: (mine_cvg_0_cvg_0 lte01) => // n; rewrite mule_ge0. Qed. Lemma hahn_decomposition_lemma : measurable D -> @@ -942,10 +938,11 @@ Proof. by move=> U mU; rewrite fin_num_measure. Qed. HB.instance Definition _ := @Measure_isFinite.Build _ _ _ jordan_neg finite_jordan_neg. -Lemma jordan_decomp (A : set T) (mA : measurable A) : +Lemma jordan_decomp (A : set T) : measurable A -> nu A = (cadd [the charge _ _ of jordan_pos] ([the charge _ _ of cscale (-1) [the charge _ _ of jordan_neg]])) A. Proof. +move=> mA. rewrite caddE cjordan_posE /= cscaleE EFinN mulN1e cjordan_negE oppeK. rewrite /crestr0 mem_set// -[in LHS](setIT A). case: nuPN => _ _ <- PN0; rewrite setIUr chargeU//. @@ -1595,18 +1592,18 @@ exists f; split. - apply/integrableP; split; first exact: ge0_emeasurable_fun_sum. 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. +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 -> @@ -1625,13 +1622,13 @@ move/integrableP : fi => [mf fi]. have mg : measurable_fun [set: T] g. apply: measurable_fun_ifT => //; apply: (measurable_fun_bool true) => /=. by have := emeasurable_fin_num measurableT mf; rewrite setTI. -exists g; split => //. -- by move=> x; rewrite /g; case: ifPn. -- by move=> x; rewrite /g; case: ifPn. +exists g; split => // [x|x| |A mA]. +- by rewrite /g; case: ifPn. +- by rewrite /g; case: ifPn. - apply/integrableP; split => //; apply/abse_integralP => //. move/ae_eq_integral : (fg) => /(_ measurableT mf) <-//. exact/abse_integralP. -- move=> A mA; rewrite nuf ?inE//; apply: ae_eq_integral => //. +- rewrite nuf ?inE//; apply: ae_eq_integral => //. + exact: measurable_funTS. + exact: measurable_funTS. + exact: ae_eq_subset fg. @@ -1651,26 +1648,18 @@ Definition f : T -> \bar R := | right _ => cst -oo end. -Theorem f_ge0 : nu `<< mu -> forall x, 0 <= f x. -Proof. -by move=> numu; rewrite /f; case: pselect => // {}numu; case: cid => x []. -Qed. +Lemma f_ge0 : nu `<< mu -> forall x, 0 <= f x. +Proof. by rewrite /f; case: pselect => // numu _; case: cid => x []. Qed. -Theorem f_fin_num : nu `<< mu -> forall x, f x \is a fin_num. -Proof. -by move=> numu; rewrite /f; case: pselect => // {}numu; case: cid => x []. -Qed. +Lemma f_fin_num : nu `<< mu -> forall x, f x \is a fin_num. +Proof. by rewrite /f; case: pselect => // numu _; case: cid => x []. Qed. -Theorem f_integrable : nu `<< mu -> mu.-integrable [set: T] f. -Proof. -by move=> numu; rewrite /f; case: pselect => // {}numu; case: cid => x []. -Qed. +Lemma f_integrable : nu `<< mu -> mu.-integrable [set: T] f. +Proof. by rewrite /f; case: pselect => // numu _; case: cid => x []. Qed. -Theorem f_integral : nu `<< mu -> forall A, measurable A -> +Lemma f_integral : nu `<< mu -> forall A, measurable A -> nu A = \int[mu]_(x in A) f x. -Proof. -by move=> numu; rewrite /f; case: pselect => // {}numu; case: cid => x []. -Qed. +Proof. by rewrite /f; case: pselect => // numu _; case: cid => x []. Qed. End radon_nikodym_sigma_finite_def. @@ -1683,17 +1672,17 @@ Implicit Types f : T -> \bar R. Local Notation "'d nu '/d mu" := (f nu mu). -Lemma change_of_variables f : (forall x, 0 <= f x) -> - forall E, measurable E -> measurable_fun E f -> +Lemma change_of_variables f E : (forall x, 0 <= f x) -> + measurable E -> measurable_fun E f -> \int[mu]_(x in E) (f x * ('d nu '/d mu) x) = \int[nu]_(x in E) f x. Proof. -move=> f0 E mE mf; set g := 'd nu '/d mu. +move=> f0 mE mf; set g := 'd nu '/d mu. have [h [ndh hf]] := approximation mE mf (fun x _ => f0 x). 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. - under eq_integral. by move=> x /[!inE] Ex; rewrite fE //; over. + under eq_integral => x /[!inE] /fE -> //. apply: monotone_convergence => //. - move=> n; apply/EFin_measurable_fun. by apply: (measurable_funS measurableT) => //; exact/measurable_funP. @@ -1704,7 +1693,7 @@ have -> : \int[mu]_(x in E) (f \* g) x = 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]. - under eq_integral. by move=> x /[!inE] Ex; rewrite fg //; over. + under eq_integral => x /[!inE] /fg -> //. apply: monotone_convergence => [//| | |]. - move=> n; apply/emeasurable_funM; apply/measurable_funTS. exact/EFin_measurable_fun. @@ -1713,7 +1702,7 @@ have -> : \int[mu]_(x in E) (f \* g) x = - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin// f_ge0. 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. - under eq_fun. by move=> n; rewrite suf; over. by []. + by under eq_fun do rewrite suf. transitivity (\int[nu]_(x in E) (\sum_(y \in range (h n)) (y * \1_(h n @^-1` [set y]) x)%:E)); last first. by apply: eq_integral => t tE; rewrite /= fimfunE -fsumEFin. @@ -1723,43 +1712,35 @@ rewrite ge0_integral_fsum//; last by move=> m y Ey; exact: nnfun_muleindic_ge0. transitivity (\int[mu]_(x in E) (\sum_(y \in range (h n)) (y * \1_(h n @^-1` [set y]) x)%:E * g x)). under [RHS]eq_integral => x xE. - rewrite -ge0_mule_fsuml; last first. - by move=> y; exact: nnfun_muleindic_ge0. + rewrite -ge0_mule_fsuml => [|y]; last exact: nnfun_muleindic_ge0. rewrite fsumEFin // -(fimfunE _ x); over. by []. rewrite ge0_integral_fsum//; last 2 first. - move=> y; apply: emeasurable_funM => //; apply: measurable_funTS. exact: measurable_int (f_integrable _). - - by move=> m y Ey; rewrite mule_ge0//; [exact: nnfun_muleindic_ge0| - exact: f_ge0]. + - by move=> m y Ey; rewrite mule_ge0 ?f_ge0// nnfun_muleindic_ge0. apply: eq_fsbigr => r rhn. under [RHS]eq_integral do rewrite EFinM. rewrite integralZl_indic_nnsfun => //. -under [LHS]eq_integral do rewrite EFinM -muleA. +under eq_integral do rewrite EFinM -muleA. rewrite ge0_integralZl//. - suff intE1 F : measurable F -> \int[nu]_(x in E) (EFin \o \1_F) x = - \int[mu]_(x in E) ((EFin \o \1_F) x * g x). - by rewrite intE1. - move=> mF /=. - under eq_integral. - by move=> x xE; rewrite -[_%:E]mul1e -/(idfun 1); over. - rewrite -(integral_setI_indic _ _)//. - transitivity (\int[mu]_(x in E `&` F) g x). - rewrite -f_integral//=; last exact: measurableI. - by rewrite integral_cst ?mul1e//; exact: measurableI. - by rewrite integral_setI_indic//; under eq_integral do rewrite muleC. + congr *%E. + under eq_integral do rewrite muleC. + under [RHS]eq_integral do rewrite -[_%:E]mul1e -/(idfun 1). + rewrite -(integral_setI_indic _ _)// -(integral_setI_indic _ _)//. + by rewrite -f_integral//= integral_cst ?mul1e. - apply: emeasurable_funM; first exact/EFin_measurable_fun. - by apply: measurable_funTS => //; exact: measurable_int (f_integrable _). + exact/measurable_funTS/(measurable_int (f_integrable _)). - by move=> t Et; rewrite mule_ge0// ?lee_fin//; exact: f_ge0. - by move: rhn; rewrite inE => -[t _ <-]; rewrite lee_fin. Qed. -Lemma integrableM f : (forall x, 0 <= f x) -> forall E, measurable E -> +Lemma integrableM f E : (forall x, 0 <= f x) -> measurable E -> nu.-integrable E f -> mu.-integrable E (f \* 'd nu '/d mu). Proof. -move=> f0 E mE intEf; apply/integrableP; split. +move=> f0 mE intEf; apply/integrableP; split. apply: emeasurable_funM; first exact: (@measurable_int _ _ _ nu). - by apply: measurable_funTS; exact: measurable_int (f_integrable _). + exact/measurable_funTS/(measurable_int (f_integrable _)). under eq_integral. move=> x _; rewrite gee0_abs; last first. by apply: mule_ge0=> //; exact: f_ge0. @@ -1778,19 +1759,19 @@ Variables (nu : {finite_measure set T -> \bar R}) Local Notation "'d nu '/d mu" := (f nu mu). -Lemma chain_rule : nu `<< mu -> mu `<< la -> forall E, measurable E -> +Lemma chain_rule E : nu `<< mu -> mu `<< la -> measurable E -> ae_eq la E ('d nu '/d la) ('d nu '/d mu \* 'd mu '/d la). Proof. -move=> numu mula E mE; have nula := measure_dominates_trans numu mula. +move=> numu mula mE; have nula := measure_dominates_trans numu mula. have mf : measurable_fun E ('d nu '/d mu). - by apply: measurable_funTS; exact: measurable_int (f_integrable _). + exact/measurable_funTS/(measurable_int (f_integrable _)). have [h [ndh hf]] := approximation mE mf (fun x _ => f_ge0 numu x). apply: integral_ae_eq => //. - apply: (integrableS measurableT) => //. apply: f_integrable. exact: (measure_dominates_trans numu mula). -- apply: emeasurable_funM => //; apply: measurable_funTS. - exact: measurable_int (f_integrable _). +- apply: emeasurable_funM => //. + exact/measurable_funTS/(measurable_int (f_integrable _)). - move=> A AE mA; rewrite change_of_variables//. + by rewrite -!f_integral. + exact: f_ge0. @@ -1806,9 +1787,9 @@ Variables (nu : {charge set T -> \bar R}) (mu : {sigma_finite_measure set T -> \bar R}). Local Lemma Radon_Nikodym0 : nu `<< mu -> - exists2 f : T -> \bar R, (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. + exists f : T -> \bar R, [/\ (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 [P [N nuPN]] := Hahn_decomposition nu. have [fp [fp0 fpfin intfp fpE]] := @radon_nikodym_sigma_finite_fin_num _ _ _ mu @@ -1817,8 +1798,8 @@ have [fp [fp0 fpfin intfp fpE]] := @radon_nikodym_sigma_finite_fin_num _ _ _ mu have [fn [fn0 fnfin intfn fnE]] := @radon_nikodym_sigma_finite_fin_num _ _ _ mu [the {finite_measure set _ -> \bar _} of jordan_neg nuPN] (jordan_neg_dominates nuPN nu_mu). -exists (fp \- fn); first by move=> x; rewrite fin_numB// fpfin fnfin. -split; first exact: integrableB. +exists (fp \- fn); split; first by move=> x; rewrite fin_numB// fpfin fnfin. + exact: integrableB. move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//; [|exact: (integrableS measurableT)..]. rewrite -fpE ?inE// -fnE ?inE//= caddE jordan_posE jordan_negE. @@ -1827,36 +1808,29 @@ Qed. Definition Radon_Nikodym : T -> \bar R := match pselect (nu `<< mu) with - | left nu_mu => sval (cid2 (Radon_Nikodym0 nu_mu)) + | left nu_mu => sval (cid (Radon_Nikodym0 nu_mu)) | right _ => cst -oo end. Lemma Radon_NikodymE (numu : nu `<< mu) : - Radon_Nikodym = sval (cid2 (Radon_Nikodym0 numu)). + Radon_Nikodym = sval (cid (Radon_Nikodym0 numu)). Proof. rewrite /= /Radon_Nikodym; case: pselect => //= numu'. -by congr (sval (cid2 (Radon_Nikodym0 _))); exact: Prop_irrelevance. +by congr (sval (cid (Radon_Nikodym0 _))); exact: Prop_irrelevance. Qed. -Theorem Radon_Nikodym_fin_num : nu `<< mu -> - forall x, Radon_Nikodym x \is a fin_num. -Proof. -move=> numu; rewrite /Radon_Nikodym; case: pselect => // {}numu. -by case: cid2. -Qed. +Lemma Radon_Nikodym_fin_num x : nu `<< mu -> + Radon_Nikodym x \is a fin_num. +Proof. by move=> numu; rewrite (Radon_NikodymE numu); case: cid => ? []. Qed. -Theorem Radon_Nikodym_integrable : nu `<< mu -> +Lemma Radon_Nikodym_integrable : nu `<< mu -> mu.-integrable [set: T] Radon_Nikodym. -Proof. -move=> numu; rewrite /Radon_Nikodym; case: pselect => // {}numu. -by case: cid2 => ? ? []. -Qed. +Proof. by move=> numu; rewrite (Radon_NikodymE numu); case: cid => ? []. Qed. -Theorem Radon_Nikodym_integral : nu `<< mu -> - forall A, measurable A -> nu A = \int[mu]_(x in A) Radon_Nikodym x. +Lemma Radon_Nikodym_integral A : nu `<< mu -> + measurable A -> nu A = \int[mu]_(x in A) Radon_Nikodym x. Proof. -move=> numu; rewrite /Radon_Nikodym; case: pselect => // {}numu. -by case: cid2 => ? ? []. +by move=> numu; rewrite (Radon_NikodymE numu); case: cid => ? [? ?]; exact. Qed. End radon_nikodym. @@ -1872,6 +1846,7 @@ Context d (T : measurableType d) (R : realType). Variables (nu : {finite_measure set T -> \bar R}) (mu : {sigma_finite_measure set T -> \bar R}). Hypothesis numu : nu `<< mu. +Implicit Types f : T -> \bar R. Lemma ae_eq_Radon_Nikodym_SigmaFinite E : measurable E -> ae_eq mu E (Radon_Nikodym_SigmaFinite.f nu mu) @@ -1885,50 +1860,38 @@ move=> mE; apply: integral_ae_eq => //. by rewrite -Radon_Nikodym_SigmaFinite.f_integral. Qed. -End Radon_Nikodym_charge_of_finite_measure. - -Section Radon_Nikodym_change_of_variables. -Context d (T : measurableType d) (R : realType). -Variables (nu : {finite_measure set T -> \bar R}) - (mu : {sigma_finite_measure set T -> \bar R}). -Hypothesis numu : nu `<< mu. -Implicit Types f : T -> \bar R. - Lemma Radon_Nikodym_change_of_variables f E : measurable E -> nu.-integrable E f -> - \int[mu]_(x in E) (f x * ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu) x) = + \int[mu]_(x in E) + (f x * ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu) x) = \int[nu]_(x in E) f x. Proof. move=> mE mf; rewrite [in RHS](funeposneg f) integralB //; last 2 first. - exact: integrable_funepos. - exact: integrable_funeneg. -transitivity (\int[mu]_(x in E) (f \* (Radon_Nikodym_SigmaFinite.f nu mu)) x). - apply: ae_eq_integral => //. - - apply: emeasurable_funM => //; last exact: measurable_funTS. - exact: measurable_int mf. - - apply: emeasurable_funM => //; first exact: measurable_int mf. - apply: measurable_funTS. - exact: measurable_int (Radon_Nikodym_SigmaFinite.f_integrable _). - - exact/ae_eq_mul2l/ae_eq_sym/ae_eq_Radon_Nikodym_SigmaFinite. -transitivity (\int[mu]_(x in E) (f^\+ \* (Radon_Nikodym_SigmaFinite.f nu mu) \- - f^\- \* (Radon_Nikodym_SigmaFinite.f nu mu)) x). - apply: eq_integral => x /[!inE] Ex. - rewrite [in LHS](funeposneg f) muleBl//=. +rewrite -(ae_eq_integral _ _ _ _ _ + (ae_eq_mul2l f (ae_eq_Radon_Nikodym_SigmaFinite mE)))//; last 2 first. +- apply: emeasurable_funM => //; first exact: measurable_int mf. + apply: measurable_funTS. + exact: measurable_int (Radon_Nikodym_SigmaFinite.f_integrable _). +- apply: emeasurable_funM => //; first exact: measurable_int mf. + exact: measurable_funTS. +rewrite [in LHS](funeposneg f). +under eq_integral => x xE. rewrite muleBl; last 2 first. - exact: Radon_Nikodym_SigmaFinite.f_fin_num. - exact: add_def_funeposneg. + over. rewrite [in LHS]integralB //; last 2 first. -- apply: Radon_Nikodym_SigmaFinite.integrableM => //. +- apply: Radon_Nikodym_SigmaFinite.integrableM => //. exact: integrable_funepos. - apply: Radon_Nikodym_SigmaFinite.integrableM => //. exact: integrable_funeneg. -congr (_ - _). -- rewrite Radon_Nikodym_SigmaFinite.change_of_variables//. - by apply: measurable_int; exact: integrable_funepos mf. -- rewrite Radon_Nikodym_SigmaFinite.change_of_variables//. - by apply: measurable_int; exact: integrable_funeneg mf. +congr (_ - _) ; rewrite Radon_Nikodym_SigmaFinite.change_of_variables//; + apply: measurable_int; first exact: integrable_funepos mf. +exact: integrable_funeneg mf. Qed. -End Radon_Nikodym_change_of_variables. +End Radon_Nikodym_charge_of_finite_measure. Section radon_nikodym_lemmas. Context d (T : measurableType d) (R : realType). @@ -1956,10 +1919,10 @@ Lemma Radon_Nikodym_cadd mu nu0 nu1 E : measurable E -> Proof. move=> mE nu0mu nu1mu; apply: integral_ae_eq => [//| | |A AE mA]. - apply: (integrableS measurableT) => //. - by apply: Radon_Nikodym_integrable => /=; exact: dominates_caddl. + by apply: Radon_Nikodym_integrable => /=; exact: dominates_cadd. - by apply: measurable_funTS => //; exact: emeasurable_funD. - rewrite integralD //; [|exact: integrableS (Radon_Nikodym_integrable _)..]. - rewrite -Radon_Nikodym_integral //=; last exact: dominates_caddl. + rewrite -Radon_Nikodym_integral //=; last exact: dominates_cadd. by rewrite -Radon_Nikodym_integral // -Radon_Nikodym_integral. Qed. @@ -1977,9 +1940,8 @@ Lemma Radon_Nikodym_chain_rule : nu `<< mu -> mu `<< la -> Proof. have [Pnu [Nnu nuPN]] := Hahn_decomposition nu. move=> numu mula; have nula := measure_dominates_trans numu mula. -apply: integral_ae_eq => //. +apply: integral_ae_eq; [exact: measurableT| |exact: emeasurable_funM|]. - exact: Radon_Nikodym_integrable. -- exact: emeasurable_funM. - move=> E _ mE. rewrite -Radon_Nikodym_integral// Radon_Nikodym_change_of_variables//. + exact: Radon_Nikodym_integral. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 0f8301973..a51e63bf3 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4335,8 +4335,7 @@ Proof. move=> fi mg fg; have mf := measurable_int fi; have gi : mu.-integrable D g. apply/integrableP; split => //; apply/abse_integralP => //; rewrite -fg//. by apply/abse_integralP => //; case/integrableP : fi. -have mugf : mu (D `&` [set x | g x < f x]) = 0. - by apply: integral_measure_lt. +have mugf : mu (D `&` [set x | g x < f x]) = 0 by apply: integral_measure_lt. have mufg : mu (D `&` [set x | f x < g x]) = 0. by apply: integral_measure_lt => // E ED mE; rewrite fg. have h : ~` [set x | D x -> f x = g x] = D `&` [set x | f x != g x]. diff --git a/theories/sequences.v b/theories/sequences.v index c5803f14d..d47856e70 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -2065,22 +2065,18 @@ have : 0 < minr e%:num r by rewrite lt_minr// r0 andbT. move/cvgrPdist_lt : minr_cvg => /[apply] -[M _ hM]. near=> n; rewrite sub0r normrN. have /hM : (M <= n)%N by near: n; exists M. -rewrite sub0r normrN (ger0_norm (u0 n)) ger0_norm//; last first. - by rewrite le_minr u0 ltW. -by move/lt_min_lt. +rewrite sub0r normrN (ger0_norm (u0 n)) ger0_norm// => [/lt_min_lt//|]. +by rewrite le_minr u0 ltW. Unshelve. all: by end_near. Qed. Lemma maxr_cvg_0_cvg_0 u r : r < 0 -> (forall k, u k <= 0) -> maxr (u n) r @[n --> \oo] --> (0:R) -> u --> (0:R). Proof. -move=> r0 u0. -under eq_fun do rewrite -(opprK (u _)) -{1}(opprK r) -oppr_min. -rewrite -oppr0. -move/cvgNP/minr_cvg_0_cvg_0. -rewrite -oppr0 ltr_oppr in r0. -move/(_ r0). +rewrite -[in r < _]oppr0 ltr_oppr => r0 u0. +under eq_fun do rewrite -(opprK (u _)) -[in maxr _ _](opprK r) -oppr_min. +rewrite -[in _ --> _]oppr0 => /cvgNP/minr_cvg_0_cvg_0-/(_ r0). have Nu0 k : 0 <= - u k by rewrite ler_oppr oppr0. -by move=> /(_ Nu0)/cvgNP; rewrite opprK. +by move=> /(_ Nu0)/(cvgNP _ _).2; rewrite opprK oppr0. Qed. End minr_cvg_0. @@ -2135,44 +2131,33 @@ Lemma maxe_cvg_0_cvg_fin_num u x : x < 0 -> (forall k, u k <= 0) -> maxe (u n) x @[n --> \oo] --> 0 -> \forall n \near \oo, u n \is a fin_num. Proof. -move=> x0 u0. -under eq_fun do rewrite -(oppeK (u _)) -{1}(oppeK x) -oppe_min. -rewrite -oppe0. -move/cvgeNP/mine_cvg_0_cvg_fin_num. -rewrite -oppe0 lte_oppr in x0. -move/(_ x0). +rewrite -[in x < _]oppe0 lte_oppr => x0 u0. +under eq_fun do rewrite -(oppeK (u _)) -[in maxe _ _](oppeK x) -oppe_min. +rewrite -[in _ --> _]oppe0 => /cvgeNP/mine_cvg_0_cvg_fin_num-/(_ x0). have Nu0 k : 0 <= - u k by rewrite lee_oppr oppe0. -move=> /(_ Nu0)[n _ Hn]. -by exists n => // k nk; rewrite -fin_numN; exact: Hn. +by move=> /(_ Nu0)[n _ nu]; exists n => // m/= nm; rewrite -fin_numN nu. Qed. Lemma maxe_cvg_maxr_cvg u r : (r < 0)%R -> (forall k, u k <= 0) -> maxe (u n) r%:E @[n --> \oo] --> 0 -> maxr (fine (u n)) r @[n --> \oo] --> (0:R)%R. Proof. -move=> r0 u0. -under eq_fun do rewrite -(oppeK (u _)) -{1}(oppeK r%:E) -oppe_min. -rewrite -oppr0 EFinN. -move/cvgeNP/mine_cvg_minr_cvg. -rewrite -oppr0 ltr_oppr in r0. -move/(_ r0). +rewrite -[in (r < _)%R]oppr0 ltr_oppr => r0 u0. +under eq_fun do rewrite -(oppeK (u _)) -[in maxe _ _](oppeK r%:E) -oppe_min. +rewrite -[in _ --> _]oppe0 => /cvgeNP/mine_cvg_minr_cvg-/(_ r0). have Nu0 k : 0 <= - u k by rewrite lee_oppr oppe0. -move=> /(_ Nu0)/cvgNP. +move=> /(_ Nu0)/(cvgNP _ _).2; rewrite oppr0. by under eq_cvg do rewrite /GRing.opp /= oppr_min fineN !opprK. Qed. Lemma maxe_cvg_0_cvg_0 u x : x < 0 -> (forall k, u k <= 0) -> maxe (u n) x @[n --> \oo] --> 0 -> u --> 0. Proof. -move=> x0 u0. -under eq_fun do rewrite -(oppeK (u _)) -{1}(oppeK x) -oppe_min. -rewrite -oppe0. -move/cvgeNP/mine_cvg_0_cvg_0. -rewrite -oppe0 lte_oppr in x0. -move/(_ x0). +rewrite -[in x < _]oppe0 lte_oppr => x0 u0. +under eq_fun do rewrite -(oppeK (u _)) -[in maxe _ _](oppeK x) -oppe_min. +rewrite -[in _ --> _]oppe0 => /cvgeNP/mine_cvg_0_cvg_0-/(_ x0). have Nu0 k : 0 <= - u k by rewrite lee_oppr oppe0. -move=> /(_ Nu0)/cvgeNP. -by under eq_cvg do rewrite oppeK. +by move=> /(_ Nu0); rewrite -[in _ --> _]oppe0 => /cvgeNP. Qed. End mine_cvg_0. From b9376bbba79bb71392efb4c3b3ef82ed30e095c2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 26 Dec 2023 19:17:23 +0900 Subject: [PATCH 07/13] fix --- CHANGELOG_UNRELEASED.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f07addd8a..03ab9d18b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -70,7 +70,7 @@ + lemma `Radon_Nikodym_sigma_finite_fin_num` + module `Radon_Nikodym_SigmaFinite` * definition `f` - * lemmas `f_ge0`, `f_fin_num`, `f_integrable`, `f_integral` + * lemmas `f_ge0`, `f_fin_num`, `f_integrable`, `f_integral` * lemma `change_of_variables` * lemma `integrableM` * lemma `chain_rule` From 314ec4f5afe79077827cb7a54412d093a25f305b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 26 Dec 2023 19:19:26 +0900 Subject: [PATCH 08/13] fix --- CHANGELOG_UNRELEASED.md | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 03ab9d18b..5511a9de6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -68,12 +68,6 @@ + lemma `cjordan_negE` + lemma `jordan_negE` + lemma `Radon_Nikodym_sigma_finite_fin_num` - + module `Radon_Nikodym_SigmaFinite` - * definition `f` - * lemmas `f_ge0`, `f_fin_num`, `f_integrable`, `f_integral` - * lemma `change_of_variables` - * lemma `integrableM` - * lemma `chain_rule` + lemma `Radon_Nikodym_fin_num` + lemma `Radon_Nikodym_integral` + lemma `ae_eq_Radon_Nikodym_SigmaFinite` @@ -114,7 +108,9 @@ - in `charge.v` + definition `jordan_decomp` now uses `cadd` and `cscale` - + Definition `Radon_Nikodym_SigmaFinite` now be a module `Radon_Nikodym_SigmaFinite` with + + definition `Radon_Nikodym_SigmaFinite` now in a module `Radon_Nikodym_SigmaFinite` with + * definition `f` + * lemmas `f_ge0`, `f_fin_num`, `f_integrable`, `f_integral` * lemma `change_of_variables` * lemma `integralM` * lemma `chain_rule` From 1e4f6d58767debf1b169f314ffc662b8c96f5aec Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 27 Dec 2023 09:16:16 +0900 Subject: [PATCH 09/13] rm caddE cscaleE --- CHANGELOG_UNRELEASED.md | 2 -- theories/charge.v | 16 ++++++---------- 2 files changed, 6 insertions(+), 12 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5511a9de6..c3af81cf6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -58,9 +58,7 @@ - in `charge.v` + definition `charge_of_finite_measure` (instance of `charge`) - + lemma `cscaleE` + lemma `dominates_cscale` - + lemma `caddE` + definition `cpushforward` (instance of `charge`) + lemma `dominates_pushforward` + lemma `cjordan_posE` diff --git a/theories/charge.v b/theories/charge.v index 39c9f0905..24231bb0b 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -396,15 +396,13 @@ Qed. HB.instance Definition _ := isCharge.Build _ _ _ cscale cscale0 cscale_finite_measure_function cscale_sigma_additive. -Lemma cscaleE A : cscale A = r%:E * nu A. Proof. by []. Qed. - End charge_scale. Lemma dominates_cscale d (T : measurableType d) (R : realType) (mu : set T -> \bar R) (nu : {charge set T -> \bar R}) (c : R) : nu `<< mu -> cscale c nu `<< mu. -Proof. by move=> numu E mE /numu; rewrite cscaleE => ->//; rewrite mule0. Qed. +Proof. by move=> numu E mE /numu; rewrite /cscale => ->//; rewrite mule0. Qed. Section charge_add. Local Open Scope ereal_scope. @@ -436,8 +434,6 @@ Qed. HB.instance Definition _ := isCharge.Build _ _ _ cadd cadd0 cadd_finite cadd_sigma_additive. -Lemma caddE E : cadd E = n1 E + n2 E. Proof. by []. Qed. - End charge_add. Lemma dominates_cadd d (T : measurableType d) (R : realType) @@ -446,7 +442,7 @@ Lemma dominates_cadd d (T : measurableType d) (R : realType) nu0 `<< mu -> nu1 `<< mu -> cadd nu0 nu1 `<< mu. Proof. -by move=> nu0mu nu1mu A mA A0; rewrite caddE nu0mu// nu1mu// adde0. +by move=> nu0mu nu1mu A mA A0; rewrite /cadd nu0mu// nu1mu// adde0. Qed. Section pushforward_charge. @@ -916,7 +912,7 @@ Local Definition cjordan_neg : {charge set T -> \bar R} := [the charge _ _ of cscale (-1) [the charge _ _ of crestr0 nu mN]]. Lemma cjordan_negE A : cjordan_neg A = - crestr0 nu mN A. -Proof. by rewrite /= cscaleE EFinN mulN1e. Qed. +Proof. by rewrite /= /cscale/= EFinN mulN1e. Qed. Let positive_set_cjordan_neg E : 0 <= cjordan_neg E. Proof. @@ -943,7 +939,7 @@ Lemma jordan_decomp (A : set T) : measurable A -> ([the charge _ _ of cscale (-1) [the charge _ _ of jordan_neg]])) A. Proof. move=> mA. -rewrite caddE cjordan_posE /= cscaleE EFinN mulN1e cjordan_negE oppeK. +rewrite /cadd cjordan_posE /= /cscale EFinN mulN1e cjordan_negE oppeK. rewrite /crestr0 mem_set// -[in LHS](setIT A). case: nuPN => _ _ <- PN0; rewrite setIUr chargeU//. - exact: measurableI. @@ -1802,8 +1798,8 @@ exists (fp \- fn); split; first by move=> x; rewrite fin_numB// fpfin fnfin. exact: integrableB. move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//; [|exact: (integrableS measurableT)..]. -rewrite -fpE ?inE// -fnE ?inE//= caddE jordan_posE jordan_negE. -by rewrite [X in _ + X]/= cscaleE EFinN mulN1e. +rewrite -fpE ?inE// -fnE ?inE//= /cadd/= jordan_posE jordan_negE. +by rewrite /cscale EFinN mulN1e. Qed. Definition Radon_Nikodym : T -> \bar R := From e43e57b28a748d007104549847e13d585374b800 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 27 Dec 2023 13:45:36 +0900 Subject: [PATCH 10/13] addressing comments by Quentin (almost done) Co-authored-by: Tragicus <96025499+Tragicus@users.noreply.github.com> --- theories/charge.v | 28 ++++++++++++---------------- theories/constructive_ereal.v | 2 +- theories/measure.v | 22 +++++++++++++--------- 3 files changed, 26 insertions(+), 26 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index 24231bb0b..d4c278bbb 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -37,9 +37,6 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* cscale r nu == charge nu scaled by a factor r : R *) (* charge_add n1 n2 == the charge corresponding to the sum of *) (* charges n1 and n2 *) -(* cpushforward nu mf == pushforward charge of nu along *) -(* measurable function f, mf is a proof that *) -(* f is measurable function *) (* charge_of_finite_measure mu == charge corresponding to a finite measure mu *) (* *) (* * Theory *) @@ -450,22 +447,20 @@ Local Open Scope ereal_scope. Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (f : T1 -> T2). Variables (R : realFieldType) (nu : {charge set T1 -> \bar R}). -Definition cpushforward (mf : measurable_fun setT f) A := nu (f @^-1` A). - Hypothesis mf : measurable_fun setT f. -Let cpushforward0 : cpushforward mf set0 = 0. -Proof. by rewrite /cpushforward preimage_set0 charge0. Qed. +Let pushforward0 : pushforward nu mf set0 = 0. +Proof. by rewrite /pushforward preimage_set0 charge0. Qed. -Let cpushforward_finite A : measurable A -> cpushforward mf A \is a fin_num. +Let pushforward_finite A : measurable A -> pushforward nu mf A \is a fin_num. Proof. move=> mA; apply: fin_num_measure. by rewrite -[X in measurable X]setTI; exact: mf. Qed. -Let cpushforward_sigma_additive : semi_sigma_additive (cpushforward mf). +Let pushforward_sigma_additive : semi_sigma_additive (pushforward nu mf). Proof. -move=> F mF tF mUF; rewrite /cpushforward preimage_bigcup. +move=> F mF tF mUF; rewrite /pushforward preimage_bigcup. apply: charge_semi_sigma_additive. - by move=> n; rewrite -[X in measurable X]setTI; exact: mf. - apply/trivIsetP => /= i j _ _ ij; rewrite -preimage_setI. @@ -473,8 +468,8 @@ apply: charge_semi_sigma_additive. - by rewrite -preimage_bigcup -[X in measurable X]setTI; exact: mf. Qed. -HB.instance Definition _ := isCharge.Build _ _ _ (cpushforward mf) - cpushforward0 cpushforward_finite cpushforward_sigma_additive. +HB.instance Definition _ := isCharge.Build _ _ _ (pushforward nu mf) + pushforward0 pushforward_finite pushforward_sigma_additive. End pushforward_charge. @@ -495,7 +490,7 @@ Section dominates_pushforward. Lemma dominates_pushforward d d' (T : measurableType d) (T' : measurableType d') (R : realType) (mu : {measure set T -> \bar R}) (nu : {charge set T -> \bar R}) (f : T -> T') (mf : measurable_fun setT f) : - nu `<< mu -> cpushforward nu mf `<< pushforward mu mf. + nu `<< mu -> pushforward nu mf `<< pushforward mu mf. Proof. by move=> numu A mA; apply: numu; rewrite -[X in measurable X]setTI; exact: mf. Qed. @@ -1900,8 +1895,8 @@ Lemma Radon_Nikodym_cscale mu nu c E : measurable E -> nu `<< mu -> Proof. move=> mE numu; apply: integral_ae_eq => [//| | |A AE mA]. - apply: (integrableS measurableT) => //. - by apply: Radon_Nikodym_integrable => /=; exact: dominates_cscale. -- by apply: measurable_funTS; exact: emeasurable_funM. + exact/Radon_Nikodym_integrable/dominates_cscale. +- exact/measurable_funTS/emeasurable_funM. - rewrite integralZl//; last first. by apply: (integrableS measurableT) => //; exact: Radon_Nikodym_integrable. rewrite -Radon_Nikodym_integral => //; last exact: dominates_cscale. @@ -1932,7 +1927,8 @@ Variables (nu : {charge set T -> \bar R}) Lemma Radon_Nikodym_chain_rule : nu `<< mu -> mu `<< la -> ae_eq la setT ('d nu '/d la) - ('d nu '/d mu \* 'd [the charge _ _ of charge_of_finite_measure mu] '/d la). + ('d nu '/d mu \* + 'd [the charge _ _ of charge_of_finite_measure mu] '/d la). Proof. have [Pnu [Nnu nuPN]] := Hahn_decomposition nu. move=> numu mula; have nula := measure_dominates_trans numu mula. diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 9ab6dd84e..070dc5075 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -594,7 +594,7 @@ Implicit Type (x : \bar R). Definition fin_num := [qualify a x : \bar R | (x != -oo) && (x != +oo)]. Fact fin_num_key : pred_key fin_num. Proof. by []. Qed. -Canonical fin_num_keyd := KeyedQualifier fin_num_key. +(*Canonical fin_num_keyd := KeyedQualifier fin_num_key.*) Lemma fin_numE x : (x \is a fin_num) = (x != -oo) && (x != +oo). Proof. by []. Qed. diff --git a/theories/measure.v b/theories/measure.v index d8a0cdb4d..9cd8b0d46 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -117,6 +117,7 @@ From HB Require Import structures. (* * Instances of measures *) (* pushforward mf m == pushforward/image measure of m by f, where mf is a *) (* proof that f is measurable *) +(* m has type set T -> \bar R. *) (* \d_a == Dirac measure *) (* msum mu n == the measure corresponding to the sum of the measures *) (* mu_0, ..., mu_{n-1} *) @@ -1652,22 +1653,25 @@ Arguments measure_bigcup {d R T} _ _. #[global] Hint Extern 0 (sigma_additive _) => solve [apply: measure_sigma_additive] : core. +Definition pushforward d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) + (R : realFieldType) (m : set T1 -> \bar R) (f : T1 -> T2) + of measurable_fun setT f := fun A => m (f @^-1` A). +Arguments pushforward {d1 d2 T1 T2 R} m {f}. + Section pushforward_measure. Local Open Scope ereal_scope. -Context d d' (T1 : measurableType d) (T2 : measurableType d') (f : T1 -> T2). -Variables (R : realFieldType) (m : {measure set T1 -> \bar R}). - -Definition pushforward (mf : measurable_fun setT f) A := m (f @^-1` A). - +Context d d' (T1 : measurableType d) (T2 : measurableType d') + (R : realFieldType). +Variables (m : {measure set T1 -> \bar R}) (f : T1 -> T2). Hypothesis mf : measurable_fun setT f. -Let pushforward0 : pushforward mf set0 = 0. +Let pushforward0 : pushforward m mf set0 = 0. Proof. by rewrite /pushforward preimage_set0 measure0. Qed. -Let pushforward_ge0 A : 0 <= pushforward mf A. +Let pushforward_ge0 A : 0 <= pushforward m mf A. Proof. by apply: measure_ge0; rewrite -[X in measurable X]setIT; apply: mf. Qed. -Let pushforward_sigma_additive : semi_sigma_additive (pushforward mf). +Let pushforward_sigma_additive : semi_sigma_additive (pushforward m mf). Proof. move=> F mF tF mUF; rewrite /pushforward preimage_bigcup. apply: measure_semi_sigma_additive. @@ -1678,7 +1682,7 @@ apply: measure_semi_sigma_additive. Qed. HB.instance Definition _ := isMeasure.Build _ _ _ - (pushforward mf) pushforward0 pushforward_ge0 pushforward_sigma_additive. + (pushforward m mf) pushforward0 pushforward_ge0 pushforward_sigma_additive. End pushforward_measure. From 822e624269ddbd44cb13267ff89da1c556283815 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 28 Dec 2023 00:36:47 +0900 Subject: [PATCH 11/13] 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. From 77b96b799f480a5415f831db0d105e5f8087e1a3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 28 Dec 2023 00:48:49 +0900 Subject: [PATCH 12/13] fix --- theories/charge.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/charge.v b/theories/charge.v index a46b48839..5fa0c469a 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1793,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. From 31419c6d33199f0e78ed8285b03b1f651af644c1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 6 Jan 2024 18:27:20 +0900 Subject: [PATCH 13/13] last comment --- CHANGELOG_UNRELEASED.md | 2 +- theories/charge.v | 15 ++++++++++++--- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9996fd5ab..814f826ef 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -58,7 +58,7 @@ - in `charge.v` + definition `charge_of_finite_measure` (instance of `charge`) - + lemma `dominates_cscale` + + lemmas `dominates_cscalel`, `dominates_cscaler` + definition `cpushforward` (instance of `charge`) + lemma `dominates_pushforward` + lemma `cjordan_posE` diff --git a/theories/charge.v b/theories/charge.v index 5fa0c469a..7d74c6bb1 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -395,12 +395,21 @@ HB.instance Definition _ := isCharge.Build _ _ _ cscale End charge_scale. -Lemma dominates_cscale d (T : measurableType d) (R : realType) +Lemma dominates_cscalel d (T : measurableType d) (R : realType) (mu : set T -> \bar R) (nu : {charge set T -> \bar R}) (c : R) : nu `<< mu -> cscale c nu `<< mu. Proof. by move=> numu E mE /numu; rewrite /cscale => ->//; rewrite mule0. Qed. +Lemma dominates_cscaler d (T : measurableType d) (R : realType) + (nu : {charge set T -> \bar R}) + (mu : set T -> \bar R) + (c : R) : c != 0%R -> mu `<< nu -> mu `<< cscale c nu. +Proof. +move=> /negbTE c0 munu E mE /eqP; rewrite /cscale mule_eq0 eqe c0/=. +by move=> /eqP/munu; exact. +Qed. + Section charge_add. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). @@ -1886,11 +1895,11 @@ Lemma Radon_Nikodym_cscale mu nu c E : measurable E -> nu `<< mu -> Proof. move=> mE numu; apply: integral_ae_eq => [//| | |A AE mA]. - apply: (integrableS measurableT) => //. - exact/Radon_Nikodym_integrable/dominates_cscale. + exact/Radon_Nikodym_integrable/dominates_cscalel. - exact/measurable_funTS/emeasurable_funM. - rewrite integralZl//; last first. by apply: (integrableS measurableT) => //; exact: Radon_Nikodym_integrable. - rewrite -Radon_Nikodym_integral => //; last exact: dominates_cscale. + rewrite -Radon_Nikodym_integral => //; last exact: dominates_cscalel. by rewrite -Radon_Nikodym_integral. Qed.