From 74b4d4f9dc39020ee0e15038aa6ba2d14b38badf Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Sat, 6 Jan 2024 18:55:52 +0900 Subject: [PATCH] Radon-Nikodym chain rule (#1083) * Radon_Nikodym chain rule --------- Co-authored-by: IshiguroYoshihiro Co-authored-by: IshiguroYoshihiro <103252572+IshiguroYoshihiro@users.noreply.github.com> Co-authored-by: Tragicus <96025499+Tragicus@users.noreply.github.com> --- CHANGELOG_UNRELEASED.md | 44 +++ theories/charge.v | 668 +++++++++++++++++++++++++--------- theories/constructive_ereal.v | 2 +- theories/lebesgue_integral.v | 15 +- theories/measure.v | 30 +- theories/sequences.v | 111 ++++++ 6 files changed, 673 insertions(+), 197 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fc967ae88..d1150813c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,6 +56,34 @@ - in file `measure.v` + add lemmas `ae_eq_subset`, `measure_dominates_ae_eq`. +- in `charge.v` + + definition `charge_of_finite_measure` (instance of `charge`) + + lemmas `dominates_cscalel`, `dominates_cscaler` + + 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` + + 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` + + 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` + + 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 `normedtype.v`: @@ -76,15 +104,31 @@ `ae_eq_mul1l`, `ae_eq_abse` +- in `charge.v` + + definition `jordan_decomp` now uses `cadd` and `cscale` + + 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` + +- in `sequences.v`: + + change the implicit arguments of `trivIset_seqDU` + ### Renamed - in `exp.v`: + `lnX` -> `lnXn` +- in `charge.v`: + + `dominates_caddl` -> `dominates_cadd` ### Generalized - 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 aae9e443c..b56ebf1f3 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -35,6 +35,9 @@ 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 *) +(* 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 *) @@ -219,6 +222,28 @@ HB.instance Definition _ := isMeasure.Build _ T R (measure_of_charge nupos) End measure_of_charge. Arguments measure_of_charge {d T R}. +Section charge_of_finite_measure. +Context d (T : measurableType d) (R : realType). +Variables (mu : {finite_measure set T -> \bar R}). + +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. + +Let nu_finite S : measurable S -> nu S \is a fin_num. +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 nu + 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}. @@ -370,12 +395,27 @@ HB.instance Definition _ := isCharge.Build _ _ _ cscale End charge_scale. +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). -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. @@ -388,9 +428,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. @@ -402,6 +442,70 @@ HB.instance Definition _ := isCharge.Build _ _ _ cadd End charge_add. +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 -> + 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 d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (f : T1 -> T2). +Variables (R : realFieldType) (nu : {charge set T1 -> \bar R}). + +Hypothesis mf : measurable_fun setT f. + +Let pushforward0 : pushforward nu mf set0 = 0. +Proof. by rewrite /pushforward preimage_set0 charge0. Qed. + +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 pushforward_sigma_additive : semi_sigma_additive (pushforward nu mf). +Proof. +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. + 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 _ _ _ (pushforward nu mf) + pushforward0 pushforward_finite pushforward_sigma_additive. + +End pushforward_charge. + +HB.builders Context d (T : measurableType d) (R : realType) + (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. + +HB.end. + +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 -> pushforward 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. @@ -416,6 +520,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. @@ -525,55 +630,14 @@ 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. +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 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. -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=> u0 h. +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 -> @@ -618,7 +682,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. @@ -822,17 +886,24 @@ 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 +912,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 /= /cscale/= 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 +938,14 @@ 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) : 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). +move=> mA. +rewrite /cadd cjordan_posE /= /cscale 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 +955,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,43 +1512,41 @@ Qed. End radon_nikodym_finite. -Section radon_nikodym. +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. +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. @@ -1494,7 +1568,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_ /=. @@ -1510,122 +1584,360 @@ 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. - 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. - -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 & - forall A, measurable A -> nu A = \int[mu]_(x in A) f x. +have ae_f := integrable_ae measurableT fi. +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 /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 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 : (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. + +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 nu_mu)) + | right _ => cst -oo + end. + +Lemma f_ge0 : nu `<< mu -> forall x, 0 <= f x. +Proof. by 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. + +Lemma f_integrable : nu `<< mu -> mu.-integrable [set: T] f. +Proof. by rewrite /f; case: pselect => // numu _; case: cid => x []. Qed. + +Lemma f_integral : nu `<< mu -> forall A, measurable A -> + nu A = \int[mu]_(x in A) f x. +Proof. by 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 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 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 => x /[!inE] /fE -> //. + 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 => x /[!inE] /fg -> //. + 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. + 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. +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 => [|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 ?f_ge0// nnfun_muleindic_ge0. +apply: eq_fsbigr => r rhn. +under [RHS]eq_integral do rewrite EFinM. +rewrite integralZl_indic_nnsfun => //. +under eq_integral do rewrite EFinM -muleA. +rewrite ge0_integralZl//. + 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. + 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 E : (forall x, 0 <= f x) -> measurable E -> + nu.-integrable E f -> mu.-integrable E (f \* 'd nu '/d mu). +Proof. +move=> f0 mE intEf; apply/integrableP; split. + apply: emeasurable_funM; first exact: (@measurable_int _ _ _ nu). + exact/measurable_funTS/(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 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 mE; have nula := measure_dominates_trans numu mula. +have mf : measurable_fun E ('d nu '/d mu). + exact/measurable_funTS/(measurable_int (f_integrable _)). +have [h [ndh hf]] := approximation mE mf (fun x _ => f_ge0 numu x). +apply: integral_ae_eq => //. +- apply: (integrableS measurableT) => //. + apply: f_integrable. + exact: (measure_dominates_trans numu mula). +- 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. + + 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 -> + 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 intfp fpE] := @radon_nikodym_sigma_finite 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 intfn fnE] := @radon_nikodym_sigma_finite 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); 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); 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//= /cadd/= jordan_posE jordan_negE. +by rewrite /cscale 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)) + | left nu_mu => sval (cid (Radon_Nikodym0 nu_mu)) | right _ => cst -oo end. -Local Notation "'d nu '/d mu" := (Radon_Nikodym mu nu). - -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). +Lemma Radon_NikodymE (numu : nu `<< mu) : + Radon_Nikodym = sval (cid (Radon_Nikodym0 numu)). Proof. -move=> numu; rewrite /Radon_Nikodym; case: pselect => // {}numu. -by case: cid2. +rewrite /= /Radon_Nikodym; case: pselect => //= numu'. +by congr (sval (cid (Radon_Nikodym0 _))); exact: Prop_irrelevance. 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. +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. + +Lemma Radon_Nikodym_integrable : nu `<< mu -> + mu.-integrable [set: T] Radon_Nikodym. +Proof. by move=> numu; rewrite (Radon_NikodymE numu); case: cid => ? []. Qed. + +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. -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. +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) + ('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. +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. +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 => //. + exact: integrable_funepos. +- apply: Radon_Nikodym_SigmaFinite.integrableM => //. + exact: integrable_funeneg. +congr (_ - _) ; rewrite Radon_Nikodym_SigmaFinite.change_of_variables//; + apply: measurable_int; first exact: integrable_funepos mf. +exact: integrable_funeneg mf. +Qed. -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). +End Radon_Nikodym_charge_of_finite_measure. + +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) => //. + 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. -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 _)..]. - rewrite -Radon_Nikodym_integral //=; last exact: dominates_caddl. + 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_cadd. +- by apply: measurable_funTS => //; exact: emeasurable_funD. +- rewrite integralD //; [|exact: integrableS (Radon_Nikodym_integrable _)..]. + rewrite -Radon_Nikodym_integral //=; last exact: dominates_cadd. 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: measurableT| |exact: emeasurable_funM|]. +- exact: Radon_Nikodym_integrable. +- 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/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/lebesgue_integral.v b/theories/lebesgue_integral.v index 4bc3cc799..a51e63bf3 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,16 @@ 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. diff --git a/theories/measure.v b/theories/measure.v index ec7f86fae..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. @@ -4498,6 +4502,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 +4514,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..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. @@ -2052,6 +2053,116 @@ 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// => [/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. +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 _ _).2; rewrite opprK oppr0. +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. +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. +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. +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 _ _).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. +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. +by move=> /(_ Nu0); rewrite -[in _ --> _]oppe0 => /cvgeNP. +Qed. + +End mine_cvg_0. + Definition sdrop T (u : T^nat) n := [set u k | k in [set k | k >= n]]%N. Section sdrop.