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.