fixes #1463 (#1663)

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -241,6 +241,22 @@
 - in `lebesgue_integral_fubiniv.`:
   + `fubini1` -> `integral12_prod_meas1`
   + `fubini2` -> `integral21_prod_meas1`
+- in `normed_module.v`:
+  + `cvgZl` -> `cvgZr_tmp`
+  + `is_cvgZl` -> `is_cvgZr_tmp`
+  + `cvgZr` -> `cvgZl_tmp`
+  + `is_cvgZr` -> `is_cvgZl_tmp`
+  + `is_cvgZrE` -> `is_cvgZlE`
+  + `cvgMl` -> `cvgMr_tmp`
+  + `cvgMr` -> `cvgMl_tmp`
+  + `is_cvgMr` -> `is_cvgMl_tmp`
+  + `is_cvgMrE` -> `is_cvgMlE_tmp`
+  + `is_cvgMl` -> `is_cvgMr_tmp`
+  + `is_cvgMlE` -> `is_cvgMrE_tmp`
+  + `limZl` -> `limZr_tmp`
+  + `limZr` -> `limZl_tmp`
+  + `continuousZr` -> `continuousZl_tmp`
+  + `continuousZl` -> `continuousZr_tmp`
 
 ### Generalized
 

theories/derive.v

@@ -322,7 +322,7 @@ apply: cvg_lim => //.
 pose g1 : R -> W := fun h => (h^-1 * h) *: 'd f a v.
 pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ).
 rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD.
-  rewrite -(scale1r (_ _ v)); apply: cvgZl => /= X [e e0].
+  rewrite -(scale1r (_ _ v)); apply: cvgZr_tmp => /= X [e e0].
   rewrite /ball_ /= => eX.
   apply/nbhs_ballP.
   by exists e => //= x _ x0; apply eX; rewrite mulVr // ?unitfE //= subrr normr0.
@@ -434,7 +434,7 @@ Fact dscale (f : V -> W) k x :
   differentiable f x -> continuous (k \*: 'd f x) /\
   (k *: f) \o shift x = cst ((k *: f) x) + k \*: 'd f x +o_ 0 id.
 Proof.
-move=> df; split; first by move=> ?; apply: continuousZr.
+move=> df; split; first by move=> ?; apply: continuousZl_tmp.
 apply/eqaddoE; rewrite funeqE => y /=.
 by rewrite -[(k *: f) _]/(_ *: _) diff_locallyx // !scalerDr scaleox.
 Qed.
@@ -447,7 +447,7 @@ Fact dscalel (k : V -> R) (f : W) x :
     cst (k x *: f) + (fun z => 'd k x z *: f) +o_ 0 id.
 Proof.
 move=> df; split.
-  move=> ?; exact/continuousZl/diff_continuous.
+  move=> ?; exact/continuousZr_tmp/diff_continuous.
 apply/eqaddoE; rewrite funeqE => y /=.
 by rewrite diff_locallyx //= !scalerDl scaleolx.
 Qed.
@@ -945,7 +945,7 @@ move=> xn0; suff: continuous (fun h : R => - (1 / x) ^+ 2 *: h) /\
   rewrite !mul1r !GRing.exprVn.
   rewrite (_ : (fun x => x^-1) =  (fun x => 1 / x ))//.
   by rewrite funeqE => y; rewrite mul1r.
-split; first by move=> ?; apply: continuousZr.
+split; first by move=> ?; exact: continuousZl_tmp.
 apply/eqaddoP => _ /posnumP[e]; near=> h.
 rewrite -[(_ + _ : R -> R) h]/(_ + _) -[(- _ : R -> R) h]/(- _) /=.
 rewrite opprD scaleNr opprK /cst /=.
@@ -1222,7 +1222,7 @@ Proof.
 move=> df; evar (h : R -> W); rewrite [X in X @ _](_ : _ = h) /=; last first.
   rewrite funeqE => r.
   by rewrite scalerBr !scalerA mulrC -!scalerA -!scalerBr /h.
-exact: cvgZr.
+exact: cvgZl_tmp.
 Qed.
 
 Lemma deriveZ f (k : R) (x v : V) : derivable f x v ->
@@ -1285,7 +1285,7 @@ evar (fg : R -> R); rewrite [X in X @ _](_ : _ = fg) /=; last first.
     by rewrite !scalerBr -addrA ![g x *: _]mulrC addKr.
   rewrite scalerDr scalerA mulrC -scalerA.
   by rewrite [_ *: (g x *: _)]scalerA mulrC -scalerA /fg.
-apply: cvgD; last exact: cvgZr df.
+apply: cvgD; last exact: cvgZl_tmp df.
 apply: cvg_comp2 (@scale_continuous _ _ (_, _)) => /=; last exact: dg.
 suff : {for 0, continuous (fun h : R => f(h *: v + x))}.
   by move=> /continuous_withinNx; rewrite scale0r add0r.

theories/exp.v

@@ -223,7 +223,7 @@ suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s).
     move=> t; rewrite /ball /= sub0r normrN => H tNZ.
     rewrite (lt_le_trans H)// ler_pdivrMr // mulr2n mulrDr mulr1.
     by rewrite ler_wpDr // subr_ge0 ltW.
-  rewrite limZr; last exact/is_cvg_seriesB/Csx.
+  rewrite limZl_tmp; last exact/is_cvg_seriesB/Csx.
   by rewrite lim_seriesB; last exact: Csx.
 apply: cvg_zero => /=.
 suff Cc : limn

theories/gauss_integral.v

@@ -110,7 +110,7 @@ Let continuous_NsqrM x : continuous (fun r : R => - (r * x) ^+ 2).
 Proof.
 move=> z; apply: cvgN => /=.
 apply: (cvg_comp (fun z => z * x) (fun z => z ^+ 2)).
-  by apply: cvgMl; exact: cvg_id.
+  by apply: cvgMr_tmp; exact: cvg_id.
 exact: exprn_continuous.
 Qed.
 
@@ -127,7 +127,7 @@ Proof.
 rewrite /u /= => y; rewrite /continuous_at.
 apply: cvgM; last exact: continuous_oneDsqrV.
 apply: continuous_comp => /=; last exact: continuous_expR.
-by apply: cvgMr; exact: continuous_oneDsqr.
+by apply: cvgMl_tmp; exact: continuous_oneDsqr.
 Qed.
 
 Definition integral01_u x := \int[mu]_(t in `[0, 1]) u x t.

theories/normedtype_theory/normed_module.v

@@ -496,25 +496,35 @@ Lemma is_cvgZ s f : cvg (s @ F) ->
   cvg (f @ F) -> cvg ((fun x => s x *: f x) @ F).
 Proof. by have := cvgP _ (cvgZ _ _); apply. Qed.
 
-Lemma cvgZl s k a : s @ F --> k -> s x *: a @[x --> F] --> k *: a.
+Lemma cvgZr_tmp s k a : s @ F --> k -> s x *: a @[x --> F] --> k *: a.
 Proof. by move=> ?; apply: cvgZ => //; exact: cvg_cst. Qed.
 
-Lemma is_cvgZl s a : cvg (s @ F) -> cvg ((fun x => s x *: a) @ F).
-Proof. by have := cvgP _ (cvgZl  _); apply. Qed.
+Lemma is_cvgZr_tmp s a : cvg (s @ F) -> cvg ((fun x => s x *: a) @ F).
+Proof. by have := cvgP _ (cvgZr_tmp  _); apply. Qed.
 
-Lemma cvgZr k f a : f @ F --> a -> k \*: f @ F --> k *: a.
-Proof. apply: cvgZ => //; exact: cvg_cst. Qed.
+Lemma cvgZl_tmp k f a : f @ F --> a -> k \*: f @ F --> k *: a.
+Proof. by apply: cvgZ => //; exact: cvg_cst. Qed.
 
-Lemma is_cvgZr k f : cvg (f @ F) -> cvg (k *: f  @ F).
-Proof. by have := cvgP _ (cvgZr  _); apply. Qed.
+Lemma is_cvgZl_tmp k f : cvg (f @ F) -> cvg (k *: f  @ F).
+Proof. by have := cvgP _ (cvgZl_tmp  _); apply. Qed.
 
-Lemma is_cvgZrE k f : k != 0 -> cvg (k *: f @ F) = cvg (f @ F).
+Lemma is_cvgZlE k f : k != 0 -> cvg (k *: f @ F) = cvg (f @ F).
 Proof.
-move=> k_neq0; rewrite propeqE; split => [/(@cvgZr k^-1)|/(@cvgZr k)/cvgP//].
+move=> k_neq0; rewrite propeqE; split => [/(@cvgZl_tmp k^-1)|/(@cvgZl_tmp k)/cvgP//].
 by under [_ \*: _]funext => x /= do rewrite scalerK//; apply: cvgP.
 Qed.
 
 End cvg_composition_normed.
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgZr_tmp`")]
+Notation cvgZl := cvgZr_tmp (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgZr_tmp`")]
+Notation is_cvgZl := is_cvgZr_tmp (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgZl_tmp`")]
+Notation cvgZr := cvgZl_tmp (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgZl_tmp`")]
+Notation is_cvgZr := is_cvgZl_tmp (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgZlE`")]
+Notation is_cvgZrE := is_cvgZlE (only parsing).
 
 Section cvg_composition_field.
 Context {K : numFieldType}  {T : Type}.
@@ -538,61 +548,77 @@ Proof. by move=> /cvgV cvf /cvf /cvgP. Qed.
 Lemma cvgM f g a b : f @ F --> a -> g @ F --> b -> (f \* g) @ F --> a * b.
 Proof. exact: cvgZ. Qed.
 
-Lemma cvgMl f a b : f @ F --> a -> (f x * b) @[x --> F] --> a * b.
-Proof. exact: cvgZl. Qed.
+Lemma cvgMr_tmp f a b : f @ F --> a -> f x * b @[x --> F] --> a * b.
+Proof. exact: cvgZr_tmp. Qed.
 
-Lemma cvgMr g a b : g @ F --> b -> (a * g x) @[x --> F] --> a * b.
-Proof. exact: cvgZr. Qed.
+Lemma cvgMl_tmp g a b : g @ F --> b -> a * g x @[x --> F] --> a * b.
+Proof. exact: cvgZl_tmp. Qed.
 
 Lemma is_cvgM f g : cvg (f @ F) -> cvg (g @ F) -> cvg (f \* g @ F).
 Proof. exact: is_cvgZ. Qed.
 
-Lemma is_cvgMr g a (f := fun=> a) : cvg (g @ F) -> cvg (f \* g @ F).
-Proof. exact: is_cvgZr. Qed.
+Lemma is_cvgMl_tmp g a (f := fun=> a) : cvg (g @ F) -> cvg (f \* g @ F).
+Proof. exact: is_cvgZl_tmp. Qed.
 
-Lemma is_cvgMrE g a (f := fun=> a) : a != 0 -> cvg (f \* g @ F) = cvg (g @ F).
-Proof. exact: is_cvgZrE. Qed.
+Lemma is_cvgMlE_tmp g a (f := fun=> a) : a != 0 -> cvg (f \* g @ F) = cvg (g @ F).
+Proof. exact: is_cvgZlE. Qed.
 
-Lemma is_cvgMl f a (g := fun=> a) : cvg (f @ F) -> cvg (f \* g @ F).
+Lemma is_cvgMr_tmp f a (g := fun=> a) : cvg (f @ F) -> cvg (f \* g @ F).
 Proof.
 move=> f_cvg; have -> : f \* g = g \* f by apply/funeqP=> x; rewrite /= mulrC.
-exact: is_cvgMr.
+exact: is_cvgMl_tmp.
 Qed.
 
-Lemma is_cvgMlE f a (g := fun=> a) : a != 0 -> cvg (f \* g @ F) = cvg (f @ F).
+Lemma is_cvgMrE_tmp f a (g := fun=> a) : a != 0 -> cvg (f \* g @ F) = cvg (f @ F).
 Proof.
 move=> a_neq0; have -> : f \* g = g \* f by apply/funeqP=> x; rewrite /= mulrC.
-exact: is_cvgMrE.
+exact: is_cvgMlE_tmp.
 Qed.
 
 End cvg_composition_field.
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMr_tmp`")]
+Notation cvgMl := cvgMr_tmp (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMl_tmp`")]
+Notation cvgMr := cvgMl_tmp (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMl_tmp`")]
+Notation is_cvgMr := is_cvgMl_tmp (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMr_tmp`")]
+Notation is_cvgMl := is_cvgMr_tmp (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMrE_tmp`")]
+Notation is_cvgMlE := is_cvgMrE_tmp (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMlE_tmp`")]
+Notation is_cvgMrE := is_cvgMlE_tmp (only parsing).
 
 Section limit_composition_normed.
 Context {K : numFieldType} {V : normedModType K} {T : Type}.
 Context (F : set_system T) {FF : ProperFilter F}.
 Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a : V).
 
 Lemma limZ s f : cvg (s @ F) -> cvg (f @ F) ->
-   lim ((fun x => s x *: f x) @ F) = lim (s @ F) *: lim (f @ F).
-Proof. by move=> ? ?; apply: cvg_lim => //; apply: cvgZ. Qed.
+  lim ((fun x => s x *: f x) @ F) = lim (s @ F) *: lim (f @ F).
+Proof. by move=> ? ?; apply: cvg_lim => //; exact: cvgZ. Qed.
 
-Lemma limZl s a : cvg (s @ F) ->
-   lim ((fun x => s x *: a) @ F) = lim (s @ F) *: a.
-Proof. by move=> ?; apply: cvg_lim => //; apply: cvgZl. Qed.
+Lemma limZr_tmp s a : cvg (s @ F) ->
+  lim ((fun x => s x *: a) @ F) = lim (s @ F) *: a.
+Proof. by move=> ?; apply: cvg_lim => //; exact: cvgZr_tmp. Qed.
 
-Lemma limZr k f : cvg (f @ F) -> lim (k *: f @ F) = k *: lim (f @ F).
-Proof. by move=> ?; apply: cvg_lim => //; apply: cvgZr. Qed.
+Lemma limZl_tmp k f : cvg (f @ F) -> lim (k *: f @ F) = k *: lim (f @ F).
+Proof. by move=> ?; apply: cvg_lim => //; exact: cvgZl_tmp. Qed.
 
 End limit_composition_normed.
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `limZr_tmp`")]
+Notation limZl := limZr_tmp (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `limZl_tmp`")]
+Notation limZr := limZl_tmp (only parsing).
 
 Section limit_composition_field.
 Context {K : numFieldType} {T : Type}.
 Context (F : set_system T) {FF : ProperFilter F}.
 Implicit Types (f g : T -> K).
 
 Lemma limM f g : cvg (f @ F) -> cvg (g @ F) ->
-   lim (f \* g @ F) = lim (f @ F) * lim (g @ F).
-Proof. by move=> ? ?; apply: cvg_lim => //; apply: cvgM. Qed.
+  lim (f \* g @ F) = lim (f @ F) * lim (g @ F).
+Proof. by move=> ? ?; apply: cvg_lim => //; exact: cvgM. Qed.
 
 End limit_composition_field.
 
@@ -603,13 +629,13 @@ Implicit Types (f g : T -> K) (a b : K).
 
 Lemma limV f : lim (f @ F) != 0 -> lim (f\^-1 @ F) = (lim (f @ F))^-1.
 Proof.
-by move=> ?; apply: cvg_lim => //; apply: cvgV => //; apply: cvgNpoint.
+by move=> ?; apply: cvg_lim => //; apply: cvgV => //; exact: cvgNpoint.
 Qed.
 
 Lemma is_cvgVE f : lim (f @ F) != 0 -> cvg (f\^-1 @ F) = cvg (f @ F).
 Proof.
 move=> ?; apply/propeqP; split=> /is_cvgV; last exact.
-by rewrite inv_funK; apply; rewrite limV ?invr_eq0//.
+by rewrite inv_funK; apply; rewrite limV ?invr_eq0.
 Qed.
 
 End cvg_composition_field_proper.
@@ -655,24 +681,28 @@ Lemma continuousZ s f x :
   {for x, continuous (fun x => s x *: f x)}.
 Proof. by move=> ? ?; apply: cvgZ. Qed.
 
-Lemma continuousZr f k x :
+Lemma continuousZl_tmp f k x :
   {for x, continuous f} -> {for x, continuous (k \*: f)}.
-Proof. by move=> ?; apply: cvgZr. Qed.
+Proof. by move=> ?; exact: cvgZl_tmp. Qed.
 
-Lemma continuousZl s a x :
+Lemma continuousZr_tmp s a x :
   {for x, continuous s} -> {for x, continuous (fun z => s z *: a)}.
-Proof. by move=> ?; apply: cvgZl. Qed.
+Proof. by move=> ?; exact: cvgZr_tmp. Qed.
 
 Lemma continuousM s t x :
   {for x, continuous s} -> {for x, continuous t} ->
   {for x, continuous (s \* t)}.
-Proof. by move=> f_cont g_cont; apply: cvgM. Qed.
+Proof. by move=> f_cont g_cont; exact: cvgM. Qed.
 
 Lemma continuousV s x : s x != 0 ->
   {for x, continuous s} -> {for x, continuous (fun x => (s x)^-1%R)}.
 Proof. by move=> ?; apply: cvgV. Qed.
 
 End local_continuity.
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `continuousZl_tmp`")]
+Notation continuousZr := continuousZl_tmp (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `continuousZr_tmp`")]
+Notation continuousZl := continuousZr_tmp (only parsing).
 
 Section cvg_fin.
 Context {R : numFieldType}.

theories/pi_irrational.v

@@ -395,7 +395,7 @@ near: n.
 have : pi * (pi * a) ^+ n / n`!%:R @[n --> \oo] --> 0.
   rewrite -[X in _ --> X](mulr0 pi).
   under eq_fun do rewrite -mulrA.
-  by apply: cvgMr; exact: exp_fact.
+  by apply: cvgMl_tmp; exact: exp_fact.
 move/cvgrPdist_lt => /(_ e e0).
 apply: filterS => n.
 rewrite sub0r normrN ger0_norm; last first.

theories/sequences.v

@@ -554,11 +554,11 @@ Lemma lim_seriesN f : cvg (series f @ \oo) ->
 Proof. by move=> cf; rewrite seriesN limN. Qed.
 
 Lemma is_cvg_seriesZ f k : cvgn (series f) -> cvgn (series (k *: f)).
-Proof. by move=> cf; rewrite seriesZ; exact: is_cvgZr. Qed.
+Proof. by move=> cf; rewrite seriesZ; exact: is_cvgZl_tmp. Qed.
 
 Lemma lim_seriesZ f k : cvgn (series f) ->
   limn (series (k *: f)) = k *: limn (series f).
-Proof. by move=> cf; rewrite seriesZ limZr. Qed.
+Proof. by move=> cf; rewrite seriesZ limZl_tmp. Qed.
 
 Lemma is_cvg_seriesD f g :
   cvgn (series f) -> cvgn (series g) -> cvgn (series (f + g)).
@@ -930,7 +930,7 @@ Proof.
 move=> Nz_lt1; apply/norm_cvg0P; pose t := (1 - `|z|).
 apply: (@squeeze_cvgr _ _ _ _ (cst 0) (t^-1 *: @harmonic R)); last 2 first.
 - exact: cvg_cst.
-- by rewrite -(scaler0 _ t^-1); exact: (cvgZr cvg_harmonic).
+- by rewrite -(scaler0 _ t^-1); exact: (cvgZl_tmp cvg_harmonic).
 near=> n; rewrite normr_ge0 normrX/= ler_pdivlMl ?subr_gt0//.
 rewrite -(@ler_pM2l _ n.+1%:R)// mulfV// [t * _]mulrC mulr_natl.
 have -> : 1 = (`|z| + t) ^+ n.+1 by rewrite addrC addrNK expr1n.
@@ -956,7 +956,7 @@ Lemma cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 ->
 Proof.
 move=> Nz_lt1; rewrite geometric_seriesE ?lt_eqF 1?ltr_normlW//.
 have -> : a / (1 - z) = (a * (1 - 0)) / (1 - z) by rewrite subr0 mulr1.
-by apply: cvgMl; apply: cvgMr; apply: cvgB; [apply: cvg_cst|apply: cvg_expr].
+by apply: cvgMr_tmp; apply: cvgMl_tmp; apply: cvgB; [apply: cvg_cst|apply: cvg_expr].
 Qed.
 
 Lemma cvg_geometric_series_half (R : archiFieldType) (r : R) n :
@@ -1117,7 +1117,7 @@ Let S0 N n := (N ^ N)%:R * \sum_(N.+1 <= i < n) (x / N%:R) ^+ i.
 
 Let is_cvg_S0 N : x < N%:R -> cvgn (S0 N).
 Proof.
-move=> xN; apply: is_cvgZr; rewrite is_cvg_series_restrict exprn_geometric.
+move=> xN; apply: is_cvgZl_tmp; rewrite is_cvg_series_restrict exprn_geometric.
 apply/is_cvg_geometric_series; rewrite normrM normfV.
 by rewrite ltr_pdivrMr ?mul1r !ger0_norm // 1?ltW // (lt_trans x0).
 Qed.
@@ -2809,7 +2809,7 @@ rewrite eqOP; split => [|Bf].
   by near: M.
 Unshelve. all: by end_near. Qed.
 
-(* TODO: to be changed once PR#1107 is integrated, and the following put in evt.v *)
+(* TODO: to be changed once PR#1107 is integrated, and the following put in tvs.v *)
 
 (* Definition bounded_top (K: realType) (E : normedModType K) (B : set E) :=
 forall (U : set E), nbhs 0 U ->