From 4b8abd59bab81fb34ec9c2b752cd5954e401cc83 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 19 Dec 2024 19:25:44 +0900 Subject: [PATCH] renaming --- CHANGELOG_UNRELEASED.md | 5 ++++- theories/all_analysis.v | 1 + theories/ftc.v | 4 ++-- theories/lebesgue_integral.v | 8 ++++---- theories/normedtype.v | 6 ++++-- theories/sequences.v | 4 ++-- 6 files changed, 17 insertions(+), 11 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index dec94ce93..2fca05f1b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -28,7 +28,7 @@ + lemma `abse_EFin` - in `normedtype.v`: - + lemmas `bounded_cst`, `cvgr_sub0` + + lemmas `bounded_cst`, `subr_cvg0` - in `lebesgue_integral.v`: + lemma `RintegralB` @@ -67,6 +67,9 @@ ### Renamed +- in `normedtype.v`: + + `cvge_sub0` -> `sube_cvg0` + ### Generalized ### Deprecated diff --git a/theories/all_analysis.v b/theories/all_analysis.v index 3eb98668d..b567c7690 100644 --- a/theories/all_analysis.v +++ b/theories/all_analysis.v @@ -24,3 +24,4 @@ From mathcomp Require Export convex. From mathcomp Require Export charge. From mathcomp Require Export kernel. From mathcomp Require Export pi_irrational. +From mathcomp Require Export gauss_integral. diff --git a/theories/ftc.v b/theories/ftc.v index bfb2d435a..43f98fa2a 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -151,7 +151,7 @@ have g_cvg_d1f : forall y, B y -> (g_ n y)%:E @[n --> \oo] --> (('d1 f) y a)%:E. apply/cvg_lim => //. by move: fayl; under eq_fun do rewrite scaler1. have xa0 : (forall n, x_ n - a != 0) /\ x_ n - a @[n --> \oo] --> 0. - by split=> [x|]; [rewrite subr_eq0|exact/cvgr_sub0]. + by split=> [x|]; [rewrite subr_eq0|exact/subr_cvg0]. move: fayl => /cvgr_dnbhsP/(_ _ xa0). under [in X in X -> _]eq_fun do rewrite scaler1 subrK. move=> xa_l. @@ -171,7 +171,7 @@ rewrite [X in X @ _ --> _](_ : _ = - by apply: eq_Rintegral => y _; rewrite mulrC. - rewrite /comp; under eq_fun do rewrite EFinB. by apply: integrableB => //; exact: intf. -apply/cvgr_sub0. +apply/subr_cvg0. rewrite [X in X @ _ --> _](_ : _ = (fun x => \int[mu]_(z in B) (g_ x z - ('d1 f) z a)))%R; last first. by apply/funext => n; rewrite RintegralB. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index fba3145d3..5caade897 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4463,7 +4463,7 @@ Let cvg_g_ x : D x -> g_ ^~ x @ \oo --> 0. Proof. move=> Dx; rewrite -abse0; apply: cvg_abse. move: (f_f Dx); case: (f x) => [r|/=|/=]. -- by move=> f_r; apply/cvge_sub0. +- by move=> f_r; exact/sube_cvg0. - move/cvgeyPge/(_ (fine (g x) + 1)%R) => [n _]/(_ _ (leqnn n))/= h. have : (fine (g x) + 1)%:E <= g x. by rewrite (le_trans h)// (le_trans _ (absfg n Dx))// lee_abs. @@ -4546,7 +4546,7 @@ have h n : `| \int[mu]_(x in D) f_ n x - \int[mu]_(x in D) f x | by apply: le_integrable ig => // x Dx /=; rewrite (gee0_abs (g0 Dx)) absfg. by apply: le_abse_integral => //; exact: emeasurable_funB. suff: `| \int[mu]_(x in D) f_ n x - \int[mu]_(x in D) f x | @[n \oo] --> 0. - move/cvg_abse0P/cvge_sub0; apply. + move/cvg_abse0P/sube_cvg0; apply. rewrite fin_numElt (_ : -oo = - +oo)// -lte_absl. move: dominated_integrable => /integrableP[?]; apply: le_lt_trans. by apply: (le_trans _ (@le_abse_integral _ _ _ mu D f mD _)). @@ -7182,7 +7182,7 @@ Proof. move=> mA; have := lebesgue_differentiation (locally_integrable_indic openT mA). apply: filter_app; first exact: (ae_filter_ringOfSetsType mu). apply: aeW => /= x Ax. -apply: (cvge_sub0 _ _).1 => //. +apply: (sube_cvg0 _ _).1 => //. move: Ax; rewrite /lebesgue_pt /davg /= -/mu => Ax. have : (fine (mu (ball x r)))^-1%:E * `|\int[mu]_(y in ball x r) (\1_A y - \1_A x)%:E | @[r --> 0^'+] --> 0. @@ -7284,7 +7284,7 @@ Lemma nice_lebesgue_differentiation (f : R -> R) : (fine (mu (E x n)))^-1%:E * \int[mu]_(y in E x n) (f y)%:E @[n --> \oo] --> (f x)%:E. Proof. -move=> locf x fx; apply: (cvge_sub0 _ _).1 => //=; apply/cvg_abse0P. +move=> locf x fx; apply: (sube_cvg0 _ _).1 => //=; apply/cvg_abse0P. pose r_ x : {posnum R} ^nat := (sval (cid (hE x).2)).2. pose C := (sval (cid (hE x).2)).1. have C_gt0 : (0 < C)%R by rewrite /C /sval/=; case: cid => -[? ?] []. diff --git a/theories/normedtype.v b/theories/normedtype.v index 68c4c81cd..6b7efb2e4 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2660,7 +2660,7 @@ Qed. Lemma cvg_zero f a : (f - cst a) @ F --> (0 : V) -> f @ F --> a. Proof. by move=> Cfa; apply: cvg_sub0 Cfa (cvg_cst _). Qed. -Lemma cvgr_sub0 f a : (fun x => f x - a) @ F --> 0 <-> f @ F --> a. +Lemma subr_cvg0 f a : (fun x => f x - a) @ F --> 0 <-> f @ F --> a. Proof. split=> [?|fFk]; first exact: cvg_zero. by rewrite -(@subrr _ a)//; apply: cvgB => //; exact: cvg_cst. @@ -3041,7 +3041,7 @@ Lemma cvgeB f g a b : a +? - b -> f @ F --> a -> g @ F --> b -> f \- g @ F --> a - b. Proof. by move=> ab fa gb; apply: cvgeD => //; exact: cvgeN. Qed. -Lemma cvge_sub0 f (k : \bar R) : +Lemma sube_cvg0 f (k : \bar R) : k \is a fin_num -> (fun x => f x - k) @ F --> 0 <-> f @ F --> k. Proof. move=> kfin; split. @@ -3218,6 +3218,8 @@ move=> [:apoo] [:bnoo] [:poopoo] [:poonoo]; move: a b => [a| |] [b| |] //. Unshelve. all: end_near. Qed. End ecvg_realFieldType. +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sube_cvg0`")] +Notation cvge_sub0 := sube_cvg0 (only parsing). Section max_cts. Context {R : realType} {T : topologicalType}. diff --git a/theories/sequences.v b/theories/sequences.v index 285fb6255..b3c010a90 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1827,7 +1827,7 @@ Proof. exact: is_cvgeD. Qed. Lemma __deprecated__ereal_cvg_sub0 (R : realFieldType) (f : (\bar R)^nat) (k : \bar R) : k \is a fin_num -> (fun x => f x - k) @ \oo --> 0 <-> f @ \oo --> k. -Proof. exact: cvge_sub0. Qed. +Proof. exact: sube_cvg0. Qed. Lemma __deprecated__ereal_limD (R : realFieldType) (f g : (\bar R)^nat) : cvgn f -> cvgn g -> limn f +? limn g -> @@ -1956,7 +1956,7 @@ move/cvg_ex => [[l fl||/cvg_lim fnoo]] /=; last 2 first. rewrite [X in X @ _ --> _](_ : _ = fun N => l%:E - \sum_(0 <= k < N | P k) f k). apply/cvgeNP; rewrite oppe0. under eq_fun => ? do rewrite oppeD// oppeK addeC. - exact/cvge_sub0. + exact/sube_cvg0. apply/funext => N; apply/esym/eqP; rewrite sube_eq//. by rewrite addeC -nneseries_split_cond//; exact/eqP/esym/cvg_lim. by rewrite ge0_adde_def//= ?inE; [exact: nneseries_ge0|exact: sume_ge0].