normed module identity convergence lemmas

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,13 @@
 
 ### Added
 
+- in `pseudometric_normed_Zmodule.v`:
+  + lemmas `cvg0D`, `cvgD0`, `cvg0B`, `cvgB0`, `cvgN0`
+
+- in `normed_module.v`:
+  + lemmas `cvg1M`, `cvgM1`, `cvg0M`, `cvgM0`
+  + lemmas `cvg1Z`, `cvg0Z`
+
 ### Changed
 
 ### Renamed

theories/derive.v

@@ -403,8 +403,8 @@ evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=.
 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: cvgZr_tmp => /= X [e e0].
+rewrite (_ : g = g1 + g2) ?funeqE//; apply: cvgD0.
+  apply: cvg1Z => /= X [e e0].
   rewrite /ball_ /= => eX.
   apply/nbhs_ballP.
   by exists e => //= x _ x0; apply eX; rewrite mulVf//= subrr normr0.
@@ -431,8 +431,8 @@ Qed.
 End DifferentialR_numFieldType.
 
 Section DifferentialR2.
-Variable R : numFieldType.
-Implicit Type (V : normedModType R).
+Context {R : numFieldType}.
+Implicit Type V : normedModType R.
 
 Lemma deriveEjacobian m n (f : 'rV[R]_m -> 'rV[R]_n) (a v : 'rV[R]_m) :
   differentiable f a -> 'D_ v f a = v *m jacobian f a.
@@ -1198,17 +1198,18 @@ End DeriveVW.
 Arguments derivable_cst {R V W}.
 
 Section Derive_lemmasVW.
-Variables (R : numFieldType) (V W : normedModType R).
+Context {R : numFieldType} {V W : normedModType R}.
 Implicit Types f g : V -> W.
 
 Fact der_add f g (x v : V) : derivable f x v -> derivable g x v ->
   (fun h => h^-1 *: (((f + g) \o shift x) (h *: v) - (f + g) x)) @
   0^'  --> 'D_v f x + 'D_v g x.
 Proof.
 move=> df dg.
-evar (fg : R -> W); rewrite [X in X @ _](_ : _ = fg) /=.
-  rewrite funeqE => h.
-  by rewrite !scalerDr scalerN scalerDr opprD addrACA -!scalerBr /fg.
+under [X in X @ _]eq_fun.
+  move=> /= h.
+  rewrite !scalerDr scalerN scalerDr opprD addrACA -!scalerBr.
+  over.
 exact: cvgD.
 Qed.
 
@@ -1537,7 +1538,7 @@ pose g t : R := (sup (f @` A) - f t)^-1.
 have invf_continuous : {within A, continuous g}.
   rewrite continuous_subspace_in => t tA; apply: cvgV => //=.
     by rewrite subr_eq0 gt_eqF// AfsupfA//; rewrite inE in tA.
-  by apply: cvgD; [exact: cst_continuous | apply: cvgN; exact: cf].
+  by apply: cvgD => //; apply: cvgN; exact: cf.
 have /ex_strict_bound_gt0[k k_gt0 /= imVfltk] : bounded_set (g @` A).
   exact/compact_bounded/continuous_compact.
 have [_ [t tA <-]] : exists2 y, (f @` A) y & sup (f @` A) - k^-1 < y.
@@ -2211,9 +2212,7 @@ move=> fx_lt_gx fg_neq df dg cf cg; case: ifPn => fg /=.
         h (shift x (k *: v)) @[k --> nbhs 0^'] --> h x.
       move=> ch.
       apply: cvg_comp; last exact: ch.
-      rewrite -[in nbhs x](add0r x); apply: cvgD => //.
-      rewrite -(scale0r v); apply: cvgZ => //.
-      exact: nbhs_dnbhs.
+      by apply: cvg0D => //; apply: cvg0Z; exact: nbhs_dnbhs.
     apply/(cvgr_lt (f x - g x)); last by rewrite subr_lt0.
     by apply: cvgB; exact: Hf.
   + exact: dg.

theories/gauss_integral.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import boot order ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap.
@@ -49,9 +49,7 @@ Proof. by apply: measurableT_comp => //; exact: measurableT_comp. Qed.
 Lemma continuous_gauss_fun : continuous gauss_fun.
 Proof.
 move=> x; apply: (@continuous_comp _ _ _ (fun x : R => - x ^+ 2) expR).
-  apply: cvgN; apply: (cvg_comp (fun z => z) (fun z => z ^+ 2)).
-    exact: cvg_id.
-  exact: exprn_continuous.
+  by apply: cvgN; exact: exprn_continuous.
 exact: continuous_expR.
 Qed.
 
@@ -331,15 +329,14 @@ have h_h0 x : 0 < x -> h x = h 0.
       under [X in X @ _ --> _]eq_fun do rewrite expr2.
       by apply: cvgM; apply: continuous_integral0_gauss; exact: ltW.
     by apply: derivable_within_continuous => u _; exact: derivable_integral01_u.
-  move=> c; rewrite in_itv/= => /andP[c0 cx].
-  by rewrite derive_h// mul0r => /eqP; rewrite subr_eq0 => /eqP.
+  by move=> c c0x; rewrite derive_h ?(itvP c0x)// mul0r => /subr0_eq.
 have Ig2 x : 0 < x -> (integral0_gauss x) ^+ 2 = pi / 4 - integral01_u x.
   move/h_h0/eqP; rewrite {1}/h eq_sym addrC -subr_eq => /eqP/esym.
   by rewrite h0.
 suff: pi / 4 - integral01_u x @[x --> +oo] --> pi / 4.
   apply: cvg_trans; apply: near_eq_cvg.
   by near=> x; rewrite Ig2.
-by rewrite -[in X in _ --> X](subr0 (pi / 4)); exact: cvgB.
+exact: cvgB0.
 Unshelve. end_near. Qed.
 
 End gauss_integral_proof.

theories/normedtype_theory/normed_module.v

@@ -569,17 +569,15 @@ Unshelve. all: by end_near. Qed.
 End NVS_continuity_mul.
 
 Section cvg_composition_normed.
-Context {K : numFieldType} {V : normedModType K} {T : Type}.
-Context (F : set_system T) {FF : Filter F}.
+Context {K : numFieldType} {V : normedModType K} {T : Type}
+  (F : set_system T) {FF : Filter F}.
 Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a b : V).
 
 Lemma cvgZ s f k a : s @ F --> k -> f @ F --> a ->
                      s x *: f x @[x --> F] --> k *: a.
 Proof.
 move=> ? ?; apply: continuous2_cvg => //.
-have := (@scale_continuous K V (k, a)).
-rewrite /continuous_at/=.
-exact.
+exact: (@scale_continuous K V (k, a)).
 Qed.
 
 Lemma is_cvgZ s f : cvg (s @ F) ->
@@ -589,6 +587,12 @@ Proof. by have := cvgP _ (cvgZ _ _); apply. Qed.
 Lemma cvgZr_tmp s k a : s @ F --> k -> s x *: a @[x --> F] --> k *: a.
 Proof. by move=> ?; exact: cvgZ. Qed.
 
+Lemma cvg1Z s a : s @ F --> (1 : K) -> s x *: a @[x --> F] --> a.
+Proof. by move=> ?; rewrite -[X in _ --> X]scale1r; exact: cvgZr_tmp. Qed.
+
+Lemma cvg0Z s a : s @ F --> (0 : K) -> s x *: a @[x --> F] --> 0.
+Proof. by move=> ?; rewrite -(scale0r a); exact: cvgZr_tmp. 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.
 
@@ -600,8 +604,9 @@ Proof. by have := cvgP _ (cvgZl_tmp  _); apply. Qed.
 
 Lemma is_cvgZlE k f : k != 0 -> cvg (k *: f @ F) = cvg (f @ F).
 Proof.
-move=> k_neq0; rewrite propeqE; split => [/(@cvgZl_tmp k^-1)|/(@cvgZl_tmp k)/cvgP//].
-by under [_ \*: _]funext => x /= do rewrite scalerK//; apply: cvgP.
+move=> k_neq0.
+rewrite propeqE; split => [/(@cvgZl_tmp k^-1)|/(@cvgZl_tmp k)/cvgP//].
+by under [_ \*: _]funext => x /= do rewrite scalerK//; exact: cvgP.
 Qed.
 
 End cvg_composition_normed.
@@ -623,8 +628,7 @@ Notation is_cvgZr := is_cvgZl_tmp (only parsing).
 Notation is_cvgZrE := is_cvgZlE (only parsing).
 
 Section cvg_composition_field.
-Context {K : numFieldType}  {T : Type}.
-Context (F : set_system T) {FF : Filter F}.
+Context {K : numFieldType} {T : Type} (F : set_system T) {FF : Filter F}.
 Implicit Types (f g : T -> K) (a b : K).
 
 Lemma cvgV f a : a != 0 -> f @ F --> a -> f\^-1 @ F --> a^-1.
@@ -650,6 +654,18 @@ Proof. exact: cvgZr_tmp. Qed.
 Lemma cvgMl_tmp g a b : g @ F --> b -> a * g x @[x --> F] --> a * b.
 Proof. exact: cvgZl_tmp. Qed.
 
+Lemma cvg1M f g a : f @ F --> (1 :> K) -> g @ F --> a -> f \* g @ F --> a.
+Proof. by move=> /cvgM /[apply]; rewrite mul1r. Qed.
+
+Lemma cvgM1 f g a : f @ F --> a -> g @ F --> (1 :> K) -> f \* g @ F --> a.
+Proof. by move=> /cvgM /[apply]; rewrite mulr1. Qed.
+
+Lemma cvg0M f g a : f @ F --> 0 -> g @ F --> a -> f \* g @ F --> 0.
+Proof. by move=> /cvgM /[apply]; rewrite mul0r. Qed.
+
+Lemma cvgM0 f g a : f @ F --> a -> g @ F --> 0 -> f \* g @ F --> 0.
+Proof. by move=> /cvgM /[apply]; rewrite mulr0. Qed.
+
 Lemma is_cvgM f g : cvg (f @ F) -> cvg (g @ F) -> cvg (f \* g @ F).
 Proof. exact: is_cvgZ. Qed.
 
@@ -783,17 +799,17 @@ Proof. by move=> ?; apply: cvgN. Qed.
 Lemma continuousD f g x :
   {for x, continuous f} -> {for x, continuous g} ->
   {for x, continuous (f + g)}.
-Proof. by move=> f_cont g_cont; apply: cvgD. Qed.
+Proof. by move=> ? ?; exact: cvgD. Qed.
 
 Lemma continuousB f g x :
   {for x, continuous f} -> {for x, continuous g} ->
   {for x, continuous (f - g)}.
-Proof. by move=> f_cont g_cont; apply: cvgB. Qed.
+Proof. by move=> ? ?; exact: cvgB. Qed.
 
 Lemma continuousZ s f x :
   {for x, continuous s} -> {for x, continuous f} ->
   {for x, continuous (fun x => s x *: f x)}.
-Proof. by move=> ? ?; apply: cvgZ. Qed.
+Proof. by move=> ? ?; exact: cvgZ. Qed.
 
 Lemma continuousZl_tmp f k x :
   {for x, continuous f} -> {for x, continuous (k \*: f)}.
@@ -806,11 +822,11 @@ 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; exact: cvgM. Qed.
+Proof. by move=> ? ?; 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.
+Proof. by move=> ?; exact: cvgV. Qed.
 
 End local_continuity.
 #[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `continuousZl_tmp`")]

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -1161,6 +1161,21 @@ Qed.
 Lemma is_cvgDrE f g : cvg (f @ F) -> cvg ((f + g) @ F) = cvg (g @ F).
 Proof. by rewrite addrC; apply: is_cvgDlE. Qed.
 
+Lemma cvg0D f g a : f @ F --> 0 -> g @ F --> a -> f x + g x @[x --> F] --> a.
+Proof. by move=> /cvgD /[apply]; rewrite add0r. Qed.
+
+Lemma cvgD0 f g a : f @ F --> a -> g @ F --> 0 -> f x + g x @[x --> F] --> a.
+Proof. by move=> /cvgD /[apply]; rewrite addr0. Qed.
+
+Lemma cvg0B f g a : f @ F --> 0 -> g @ F --> a -> f x - g x @[x --> F] --> -a.
+Proof. by move=> /cvgB /[apply]; rewrite add0r. Qed.
+
+Lemma cvgB0 f g a : f @ F --> a -> g @ F --> 0 -> f x - g x @[x --> F] --> a.
+Proof. by move=> /cvgB /[apply]; rewrite subr0. Qed.
+
+Lemma cvgN0 f : f @ F --> 0 -> - f @ F --> 0.
+Proof. by rewrite -{2}oppr0; exact: cvgN. Qed.
+
 Lemma cvg_sub0 f g a : (f - g) @ F --> (0 : V) -> g @ F --> a -> f @ F --> a.
 Proof.
 by move=> Cfg Cg; have := cvgD Cfg Cg; rewrite subrK add0r; apply.

theories/normedtype_theory/tvs.v

@@ -187,7 +187,7 @@ move=> x; rewrite /continuous_at.
 rewrite -(@eq_cvg _ _ _ (fun x => 0 - x)); first by move=> y; exact: add0r.
 rewrite -[- x]add0r.
 apply: (@continuous_comp _ _ _ (fun x => (0, x)) (fun x : M * M => x.1 - x.2)).
-  by apply: cvg_pair => /=; [exact: cvg_cst|exact: cvg_id].
+  exact: cvg_pair.
 exact: sub_continuous.
 Qed.
 

theories/probability_theory/beta_distribution.v

@@ -67,7 +67,7 @@ split.
 - by move=> y y01; apply: derivableM => //=; exact: onemXn_derivable.
 - apply: cvgM => //.
   apply: cvg_at_right_filter; apply: (@cvg_comp _ _ _ onem (fun x => x ^+ n)).
-    by apply: cvgB; [exact: cvg_cst|exact: cvg_id].
+    by apply: cvgB; [apply: cvg_cst|apply: cvg_id].
   exact: exprn_continuous.
 - apply: cvg_at_left_filter; apply: cvgM => //.
   apply: (@cvg_comp _ _ _ onem (fun x => x ^+ n)).

theories/probability_theory/random_variable.v

@@ -350,10 +350,10 @@ have cdf_s : cdf X r @[r --> a^'+] --> s%:E.
     by rewrite (lt_le_trans (ltNyr 0%R)) ?le_ereal_inf_tmp//= => l[? _] <-.
   rewrite (le_lt_trans _ (ltry 1%R))// ge_ereal_inf//=.
   exists (cdf X (a + 1)); last exact: cdf_le1.
-  by exists (a + 1)%R => //; rewrite in_itv /=; apply/andP; rewrite ltrDl.
+  by exists (a + 1)%R => //; rewrite in_itv/= ltrDl// ltr01/=.
 have cdf_ns : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> s%:E.
   move/cvge_at_rightP : cdf_s; apply; split=> [n|]; rewrite ?ltrDl //.
-  rewrite -[X in _ --> X]addr0; apply: cvgD => //.
+  apply: cvgD0 => //.
   by rewrite gtr0_cvgV0 ?cvg_shiftS; [near=> n | exact: cvgr_idn].
 have cdf_na : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> cdf X a.
   pose F n := X @^-1` `]-oo, (a + n.+1%:R^-1)%R].

theories/realfun.v

@@ -466,7 +466,7 @@ move=> nif; have ndNf : {in `[a, b] &, nondecreasing_fun (-%R \o f)}.
   by move=> x y xab yab xy /=; rewrite lerNl opprK nif.
 move/nondecreasing_at_left_at_right : (ndNf) => H x.
 rewrite in_itv/= => /andP[ax xb]; rewrite -[leLHS]opprK lerNl -!limN//.
-- rewrite -(opprK f);apply: is_cvgN.
+- rewrite -(opprK f); apply: is_cvgN.
   exact: nondecreasing_at_left_is_cvgrW ndNf.
 - rewrite -(opprK f); apply: is_cvgN.
   exact: nondecreasing_at_right_is_cvgrW ndNf.
@@ -2301,11 +2301,11 @@ suff /near_eq_cvg/cvg_trans : {near (- x)^'+,
 apply: filter_app (nbhs_right_lt xa).
 apply: (filter_app _ _ (nbhs_right_ge _)).
 near=> t => xt ta; have ? : -b <= t by exact: (le_trans bx).
-have ? : t <= -a by exact: ltW.
+have ? : t <= - a by exact: ltW.
 apply/eqP; rewrite eq_sym -subr_eq opprK addrC.
 rewrite /= [TV a _ f]total_variation_opp opprK -fineD.
-- by apply/bounded_variationP => //; apply: bounded_variationl bvNf.
-- by apply/bounded_variationP => //; apply: bounded_variationr bvNf.
+- by apply/bounded_variationP => //; exact: bounded_variationl bvNf.
+- by apply/bounded_variationP => //; exact: bounded_variationr bvNf.
 by rewrite -total_variationD.
 Unshelve. all: by end_near. Qed.
 
@@ -2723,8 +2723,7 @@ have f0g0 y : a < y -> y < b ->
     (f0 x - f0 y) / (g0 x - g0 y) @[x --> a^'+] --> f0 y / g0 y.
   move=> ay yb; rewrite -[X in _ --> X]opprK -mulrN -invrN -mulNr.
   apply: cvgM.
-    rewrite -[X in _ --> X]add0r; apply: cvgB => //.
-    apply: cvg_trans fa0; apply: near_eq_cvg; near=> z.
+    apply: cvg0B => //; apply: cvg_trans fa0; apply: near_eq_cvg; near=> z.
     by rewrite /f0 gt_eqF.
   apply: cvgV.
     rewrite oppr_eq0; apply/eqP => g0y0.
@@ -2736,8 +2735,7 @@ have f0g0 y : a < y -> y < b ->
     rewrite mulf_eq0// orbC gt_eqF ?subr_gt0//= => /eqP; apply/eqP.
     apply: cdg.
     by move: c0 c0ay; apply: subset_itvSoo; rewrite bnd_simp// ltW.
-  rewrite -[X in _ --> X]add0r; apply: cvgB => //.
-  apply: cvg_trans ga0; apply: near_eq_cvg; near=> z.
+  apply: cvg0B => //; apply: cvg_trans ga0; apply: near_eq_cvg; near=> z.
   by rewrite /g0 gt_eqF.
 have lfg_ub q : l < q ->
     exists2 c2, a < c2 & forall x, a < x < c2 -> f x / g x < q.