renaming

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

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.

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.

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 => -[? ?] [].

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}.

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].