From 8f3402830f9576f7a4f91c612658263a05f73a0b Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 12:59:46 +0200
Subject: [PATCH 01/17] Move `is_deriveV` and `is_derive1_comp` to `derive.v`

---
 theories/derive.v  | 18 ++++++++++++++++++
 theories/realfun.v | 19 -------------------
 2 files changed, 18 insertions(+), 19 deletions(-)

diff --git a/theories/derive.v b/theories/derive.v
index 07a7aa7cab..83fd93f025 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -1398,6 +1398,15 @@ move=> df dg; apply/cvg_ex; exists (- (f x) ^- 2 *: 'D_v f x).
 exact: der_inv.
 Qed.
 
+Lemma is_deriveV f (x v : V) (df : R) :
+  f x != 0 -> is_derive x v f df ->
+  is_derive x v (fun y => (f y)^-1) (- (f x) ^- 2 *: df).
+Proof.
+move=> fxNZ Df.
+constructor; first by apply: derivableV => //; case: Df.
+by rewrite deriveV //; case: Df => _ ->.
+Qed.
+
 End Derive_lemmasVR.
 
 Lemma derive_shift {R : numFieldType} (v k : R) :
@@ -2068,6 +2077,15 @@ rewrite diff_comp // !derive1E' //= -[X in 'd  _ _ X = _]mulr1.
 by rewrite [LHS]linearZ mulrC.
 Qed.
 
+Global Instance is_derive1_comp (R : realFieldType) (f g : R -> R) (x a b : R) :
+  is_derive (g x) 1 f a -> is_derive x 1 g b -> is_derive x 1 (f \o g) (a * b).
+Proof.
+move=> [fgxv <-{a}] [gv <-{b}]; apply: (@DeriveDef _ _ _ _ _ (f \o g)).
+  apply/derivable1_diffP/differentiable_comp; first exact/derivable1_diffP.
+  by move/derivable1_diffP in fgxv.
+by rewrite -derive1E (derive1_comp gv fgxv) 2!derive1E.
+Qed.
+
 Lemma near_eq_growth_rate (R : numFieldType) (V W : normedModType R)
     (f g : V -> W) (a v : V) : {near a, f =1 g} ->
    \forall h \near 0,
diff --git a/theories/realfun.v b/theories/realfun.v
index dd0e368af8..d2a1326c3d 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -1872,25 +1872,6 @@ apply/continuous_subspaceT=> r.
 exact/differentiable_continuous/derivable1_diffP.
 Qed.
 
-Global Instance is_derive1_comp (f g : R -> R) (x a b : R) :
-  is_derive (g x) 1 f a -> is_derive x 1 g b ->
-  is_derive x 1 (f \o g) (a * b).
-Proof.
-move=> [fgxv <-{a}] [gv <-{b}]; apply: (@DeriveDef _ _ _ _ _ (f \o g)).
-  apply/derivable1_diffP/differentiable_comp; first exact/derivable1_diffP.
-  by move/derivable1_diffP in fgxv.
-by rewrite -derive1E (derive1_comp gv fgxv) 2!derive1E.
-Qed.
-
-Lemma is_deriveV (f : R -> R) (x t v : R) :
-  f x != 0 -> is_derive x v f t ->
-  is_derive x v (fun y => (f y)^-1) (- (f x) ^- 2 *: t).
-Proof.
-move=> fxNZ Df.
-constructor; first by apply: derivableV => //; case: Df.
-by rewrite deriveV //; case: Df => _ ->.
-Qed.
-
 Lemma is_derive_inverse (f g : R -> R) l x :
   {near x, cancel f g}  ->
   {near x, continuous f}  ->

From b2536f85b330d5f12c7e66fdc57d3fafbbaa9d40 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 13:09:48 +0200
Subject: [PATCH 02/17] Utility lemmas in filter.v

---
 CHANGELOG_UNRELEASED.md |  2 ++
 classical/filter.v      | 53 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 55 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2d85fdc0a5..9522855b6e 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -126,6 +126,8 @@
 
 - in `filter.v`:
   + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType`
+  + new lemmas `near_eq_cvgE`, `near_eq_is_cvg`, `near_eq_lim`, 
+    `cvg_to_eq`, `cvg_to_withinP`, and `within_cvg_to_within`.
 
 - in `topology_structure.v`:
   + structure `SubTopological`, notation `subTopologicalType`
diff --git a/classical/filter.v b/classical/filter.v
index b26d00d72f..073ef58fdc 100644
--- a/classical/filter.v
+++ b/classical/filter.v
@@ -925,10 +925,23 @@ Lemma near_eq_cvg {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) :
   {near F, f =1 g} -> g @ F `=>` f @ F.
 Proof. by move=> eq_fg P /=; apply: filterS2 eq_fg => x /= <-. Qed.
 
+Lemma near_eq_cvgE {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) :
+  {near F, f =1 g} -> f @ F = g @ F.
+Proof.
+move=> eq_fg.
+apply/seteqP; split; apply: near_eq_cvg => //.
+by near do symmetry.
+Unshelve. all: by end_near.
+Qed.
+
 Lemma eq_cvg (T T' : Type) (F : set_system T) (f g : T -> T') (x : set_system T') :
   f =1 g -> (f @ F --> x) = (g @ F --> x).
 Proof. by move=> /funext->. Qed.
 
+Lemma near_eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') : 
+  Filter F -> {near F, g =1 f} -> cvg (f x @[x --> F]) -> cvg(g x @[x --> F]).
+Proof. by move=> /@near_eq_cvgE /[apply] ->. Qed.
+
 Lemma eq_is_cvg_in (T T' : Type) (fT : pfilteredType T') (F : set_system T) (f g : T -> T') :
   f =1 g -> [cvg (f @ F) in fT] = [cvg (g @ F) in fT].
 Proof. by move=> /funext->. Qed.
@@ -937,6 +950,14 @@ Lemma eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') :
   f =1 g -> cvg (f @ F) = cvg (g @ F).
 Proof. by move=> /funext->. Qed.
 
+Lemma near_eq_lim (T : Type) (T' : pnbhsType) {F : set_system T} {FF : Filter F} (f g : T -> T') :
+  {near F, f =1 g} -> lim (f @ F) = lim (g @ F).
+Proof. by move=> /near_eq_cvgE ->. Qed.
+
+Lemma cvg_to_eq {T : nbhsType} {F : set_system T} (l l' : T) :
+  F --> l' -> l = l' -> F --> l.
+Proof. by move=> + ->. Qed.
+
 Lemma neari_eq_loc {T U} {F : set_system T} {FF : Filter F} (f g : T -> set U) :
   {near F, f =2 g} -> g `@ F `=>` f `@ F.
 Proof.
@@ -1197,6 +1218,26 @@ Qed.
 
 End within.
 
+Lemma cvg_to_withinP (T U : Type) {F : set_system T} {FF : Filter F} {G : set_system U} {FG : Filter G} 
+    (f : T -> U) (A : set U) :
+  (f @ F --> within A G) <-> (f @ F --> G /\ \forall x \near F, A (f x)).
+Proof.
+  split.
+    move=> cvg_w; split.
+    - apply: (cvg_trans cvg_w).
+      exact: cvg_within.
+    - apply: cvg_w.
+      exact: withinT.
+  move=> [cvgT nearfA] P. 
+  rewrite !nbhs_nearE near_withinE.
+  move: cvgT => /[apply].
+  rewrite near_map appfilter nbhs_nearE => nearF_AP.
+  near=> x.
+  suff : A (f x) by near: x.
+  by near: x.
+  Unshelve. all: by end_near.
+Qed.
+
 Global Instance within_filter T D F : Filter F -> Filter (@within T D F).
 Proof.
 move=> FF; rewrite /within; constructor => /=.
@@ -1210,6 +1251,18 @@ Qed.
 Canonical within_filter_on T D (F : filter_on T) :=
   FilterType (within D F) (within_filter _ _).
 
+Lemma within_cvg_to_within (T U : Type) {F : set_system T} {FF : Filter F} {G : set_system U} {FG : Filter G}
+    (f : T -> U) (A : set T) (B : set U) :
+  (\forall x \near F, A x -> B (f x)) -> f @ F --> G -> f @ within A F --> within B G.
+Proof.
+  move=> near_hom cvgT.
+  apply/cvg_to_withinP; split.
+  - apply: cvg_trans cvgT.
+    apply: cvg_app.
+    exact: cvg_within.
+  - by rewrite near_withinE.
+Qed. 
+
 Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T)
   (F : set_system T) (P : set T) :
   Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) ->

From bfe3f74d655dd97fd8b7b3e697a11ffd83cd792b Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 13:30:19 +0200
Subject: [PATCH 03/17] New derive lemmas

- lemma `derive1Dn`
- derivation of functions of form `fun x => k x *: f x`
- derivation of shifted functions
- lemmas for near-equality of `derive1`/`derive1n`
---
 theories/derive.v | 117 +++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 116 insertions(+), 1 deletion(-)

diff --git a/theories/derive.v b/theories/derive.v
index 83fd93f025..cccec08558 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -408,6 +408,9 @@ Proof. by []. Qed.
 Lemma derive1Sn V (f : R -> V) n : f^`(n.+1) = f^`()^`(n).
 Proof. exact: iterSr. Qed.
 
+Lemma derive1Dn V (f : R -> V) (i j : nat) : f^`(i + j) = f^`(j)^`(i).
+Proof. by rewrite /derive1n iterD. Qed.
+
 End DifferentialR2.
 Notation "f ^` ()" := (derive1 f) : classical_set_scope.
 Notation "f ^` ( n )" := (derive1n n f) : classical_set_scope.
@@ -1254,6 +1257,58 @@ move=> dfx; apply: DeriveDef; first exact: derivableZ.
 by rewrite deriveZ // derive_val.
 Qed.
 
+Lemma der1_scaleLR (k : R -> R) (f : R -> V) (x : R) :
+  derivable k x 1 -> derivable f x 1 ->
+  h^-1 *: (((fun x0 : R => k x0 *: f x0) \o  shift x) h%:A - k x *: f x) 
+  @[h --> 0^'] --> 'D_1 k x *: f x + k x *: 'D_1 f x.
+Proof.
+move=> der_k der_f.
+rewrite /comp/=.
+apply: cvg_trans.
+  apply: near_eq_cvg.
+  near=> h.
+  rewrite -[X in _ = _ *: X](addrKA (- (k x *: f (h%:A + x)))) opprD opprK.
+  rewrite -scalerBl -scalerBr scalerDr [in X in _ = X + _]scalerA.
+  by rewrite scalerA (mulrC h^-1 (k x)) -[in X in _ = _ + X]scalerA.
+apply: cvgD.
+- apply: cvgZ; first exact: der_k.
+  apply: (cvg_comp _ _ (G := nbhs x)).
+  + apply: cvg0DC.
+    apply: cvg0MC.
+    by apply: cvg_within_filter.
+  + change (continuous_at x f).
+    by apply/differentiable_continuous/derivable1_diffP.
+- apply: cvgZl_tmp.
+    exact: der_f.
+Unshelve. all: by end_near. Qed.
+
+Global Instance is_derive1ZLR (k : R -> R) (f : R -> V) (x dk : R) (df : V) :
+  is_derive x 1 k dk -> is_derive x 1 f df -> is_derive x 1 (fun x => k x *: f x) (dk *: f x + k x *: df).
+Proof.
+move=> [der_k vdk] [der_f vdf].
+constructor.
+- apply: cvgP.
+  by apply: der1_scaleLR.
+- apply: norm_cvg_lim.
+  apply: cvg_to_eq; first by apply: der1_scaleLR.
+  by rewrite vdk vdf.
+Qed.
+
+Lemma deriveZLR (k : R -> R) (f : R -> V) (x : R) : 
+  derivable k x 1 -> derivable f x 1 ->
+  'D_1 (fun x => k x *: f x) x = 'D_1 k x *: f x + k x *: 'D_1 f x.
+Proof.
+move=> dk df.
+by apply: derive_val; apply: is_derive1ZLR; apply: derivableP.
+Qed.
+
+Lemma derivableZLR (k : R -> R) (f : R -> V) (x : R) : 
+  derivable k x 1 -> derivable f x 1 -> derivable (fun x => k x *: f x) x 1.
+Proof.
+move=> dk df.
+by apply: ex_derive; apply: is_derive1ZLR; apply: derivableP.
+Qed.
+
 Lemma derive_cst (k : W) (x v : V) : 'D_v (cst k) x = 0.
 Proof. by rewrite derive_val. Qed.
 
@@ -1419,6 +1474,38 @@ Lemma is_derive_shift {R : numFieldType} x v (k : R) :
   is_derive x v (shift k) v.
 Proof. by apply: DeriveDef => //; rewrite derive_val addr0. Qed.
 
+Section derive_shiftf.
+Context (R : numFieldType) (V : normedModType R) (f : R -> V).
+Implicit Types (x a v : R).
+
+Lemma derivable_shiftf x a v : 
+  derivable f (x + a) v -> derivable (f \o shift a) x v.
+Proof.
+rewrite /derivable/=.
+by under eq_is_cvg do rewrite addrA.
+Qed.
+
+Lemma derive_shiftf x a v : 
+  'D_v (f \o shift a) x = 'D_v f (x + a).
+Proof.
+  rewrite /derive/=.
+  by under [in RHS]eq_fun do rewrite addrA.
+Qed.
+
+Lemma is_derive_shiftf x a (df : V) : 
+  is_derive (x + a) 1 f df -> is_derive x 1 (f \o shift a) df.
+Proof.
+  move=> [/derivable_shiftf derf +].
+  rewrite -derive_shiftf => derf_val.
+  by constructor.
+Qed.
+
+Lemma derive1_shiftf x a : 
+  (f \o shift a)^`() x = f^`() (x + a).
+Proof. by rewrite !derive1E derive_shiftf. Qed.
+
+End derive_shiftf.
+
 Lemma derive1_cst {R : numFieldType} (V : normedModType R) (k : V) t :
   (cst k)^`() t = 0.
 Proof. by rewrite derive1E derive_cst. Qed.
@@ -1449,6 +1536,10 @@ have /= := @deriveX R R id n x v (@derivable_id _ _ _ _).
 by rewrite fctE => ->; rewrite derive_id.
 Qed.
 
+Global Instance is_derive_exp (R : numFieldType) n x v :
+  is_derive x v (@GRing.exp R ^~ n) (n%:R *: x ^+ n.-1 *: v).
+Proof. by constructor; [ exact: exprn_derivable | exact: exp_derive ]. Qed.
+
 Lemma exp_derive1 {R : numFieldType} n x :
   (@GRing.exp R ^~ n)^`() x = n%:R *: x ^+ n.-1.
 Proof. by rewrite derive1E exp_derive [LHS]mulr1. Qed.
@@ -2123,6 +2214,30 @@ move=> fg [fav <-]; rewrite (near_eq_derive _ fg).
 by apply: DeriveDef => //; exact: near_eq_derivable fav.
 Qed.
 
+Lemma near_eq_derive1n_near (R : numFieldType) (V : normedModType R) (k : nat) (f g : R -> V) (x : R) : 
+  {near x, f =1 g} -> {near x, f^`(k) =1 g^`(k)}.
+Proof.
+move=> near_eq.
+elim: k => [//|k IH].
+near=> y.
+rewrite !derive1nS !derive1E.
+apply: near_eq_derive.
+near: y.
+by rewrite near_nbhs; apply: near_join.
+Unshelve. all: by end_near. Qed.
+
+Lemma near_eq_derive1_near (R : numFieldType) (V : normedModType R) (f g : R -> V) (x : R) :
+  {near x, f =1 g} -> {near x, f^`() =1 g^`()}.
+Proof. rewrite -!derive1n1; exact: near_eq_derive1n_near. Qed.
+
+Lemma near_eq_derive1n (R : numFieldType) (V : normedModType R) (k : nat) (f g : R -> V) (x : R) : 
+  {near x, f =1 g} -> f^`(k) x = g^`(k) x.
+Proof. by move/near_eq_derive1n_near => /(_ k) /nbhs_singleton. Qed.
+
+Lemma near_eq_derive1 (R : numFieldType) (V : normedModType R) (f g : R -> V) (x : R) : 
+  {near x, f =1 g} -> f^`() x = g^`() x.
+Proof. by rewrite -!derive1n1; exact: near_eq_derive1n. Qed.
+
 Section Derive_max.
 Context {K : realType} {V W : normedModType K}.
 Implicit Types f g : V -> K^o.
@@ -2524,4 +2639,4 @@ move=> dfx dgx; apply: DiffDef; first exact: differentiable_row_mx.
 by rewrite diff_row_mx// !diff_val.
 Qed.
 
-End is_diff_row_mx.
+End is_diff_row_mx.
\ No newline at end of file

From 96d668058398831fa4762e371e784913f1f06c56 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 13:03:07 +0200
Subject: [PATCH 04/17] Update changelog

---
 CHANGELOG_UNRELEASED.md | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2d85fdc0a5..e566816a2f 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -234,6 +234,12 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in `derive.v`
+  + new lemmas `derive1Dn`, `der1_scaleLR`, `deriveZLR`, `derivableZLR`, 
+    `derivable_shiftf`, `derive_shiftf`, `is_derive_shiftf`, `derive1_shiftf`, 
+    `near_eq_derive1n_near`, `near_eq_derive1_near`, `near_eq_derive1n`, and 
+    `near_eq_derive1`.
+
 ### Changed
 
 - in `realsum.v`:
@@ -354,6 +360,9 @@
 - in `classical_sets.v`
   + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`)
 
+- moved from `realfun.v` to `derive.v`: 
+  + lemmas `is_deriveV`, `is_derive1_comp`.
+
 ### Renamed
 
 - in `tvs.v`:

From f11fbdaa38d7d6f98c7c613f9f2090a97607c8d9 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 13:40:51 +0200
Subject: [PATCH 05/17] Fix indentation

---
 classical/filter.v | 41 ++++++++++++++++++++---------------------
 1 file changed, 20 insertions(+), 21 deletions(-)

diff --git a/classical/filter.v b/classical/filter.v
index 073ef58fdc..4233a6d9bc 100644
--- a/classical/filter.v
+++ b/classical/filter.v
@@ -1222,21 +1222,20 @@ Lemma cvg_to_withinP (T U : Type) {F : set_system T} {FF : Filter F} {G : set_sy
     (f : T -> U) (A : set U) :
   (f @ F --> within A G) <-> (f @ F --> G /\ \forall x \near F, A (f x)).
 Proof.
-  split.
-    move=> cvg_w; split.
-    - apply: (cvg_trans cvg_w).
-      exact: cvg_within.
-    - apply: cvg_w.
-      exact: withinT.
-  move=> [cvgT nearfA] P. 
-  rewrite !nbhs_nearE near_withinE.
-  move: cvgT => /[apply].
-  rewrite near_map appfilter nbhs_nearE => nearF_AP.
-  near=> x.
-  suff : A (f x) by near: x.
-  by near: x.
-  Unshelve. all: by end_near.
-Qed.
+split.
+  move=> cvg_w; split.
+  - apply: (cvg_trans cvg_w).
+    exact: cvg_within.
+  - apply: cvg_w.
+    exact: withinT.
+move=> [cvgT nearfA] P. 
+rewrite !nbhs_nearE near_withinE.
+move: cvgT => /[apply].
+rewrite near_map appfilter nbhs_nearE => nearF_AP.
+near=> x.
+suff : A (f x) by near: x.
+by near: x.
+Unshelve. all: by end_near. Qed.
 
 Global Instance within_filter T D F : Filter F -> Filter (@within T D F).
 Proof.
@@ -1255,12 +1254,12 @@ Lemma within_cvg_to_within (T U : Type) {F : set_system T} {FF : Filter F} {G :
     (f : T -> U) (A : set T) (B : set U) :
   (\forall x \near F, A x -> B (f x)) -> f @ F --> G -> f @ within A F --> within B G.
 Proof.
-  move=> near_hom cvgT.
-  apply/cvg_to_withinP; split.
-  - apply: cvg_trans cvgT.
-    apply: cvg_app.
-    exact: cvg_within.
-  - by rewrite near_withinE.
+move=> near_hom cvgT.
+apply/cvg_to_withinP; split.
+- apply: cvg_trans cvgT.
+  apply: cvg_app.
+  exact: cvg_within.
+- by rewrite near_withinE.
 Qed. 
 
 Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T)

From 75a094838ef79bf40182e28f9915d37c82a637fa Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 15:43:21 +0200
Subject: [PATCH 06/17] normed module identity convergence lemmas

---
 theories/normedtype_theory/normed_module.v    | 24 ++++++++++++
 .../pseudometric_normed_Zmodule.v             | 39 +++++++++++++++++++
 2 files changed, 63 insertions(+)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 1252178b3f..94a72d0f8e 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -642,6 +642,30 @@ 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 cvg1MC f a : f @ F --> (1 :> K) -> f x * a @[x --> F] --> a.
+Proof. by move/(cvgMr_tmp (b := a)); rewrite mul1r. 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 cvgCM1 f a : f @ F --> (1 :> K) -> a * f x @[x --> F] --> a.
+Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr1. 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 cvg0MC f a : f @ F --> 0 -> f x * a @[x --> F] --> 0.
+Proof. by move/(cvgMr_tmp (b := a)); rewrite mul0r. 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 cvgCM0 f a : f @ F --> 0 -> a * f x @[x --> F] --> 0.
+Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr0. 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.
 
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 9f945624de..82c259cf1f 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -1098,6 +1098,45 @@ 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 cvgDl f a b : f @ F --> b -> a + f x @[x --> F] --> a + b.
+Proof. apply: cvgD; exact: cvg_cst. Qed.
+
+Lemma cvgDr f a b : f @ F --> a -> f x + b @[x --> F] --> a + b.
+Proof. move/cvgD; apply; exact: cvg_cst. Qed.
+
+Lemma cvgBl f a b : f @ F --> b -> a - f x @[x --> F] --> a - b.
+Proof. by move/cvgN; apply: cvgDl. Qed.
+
+Lemma cvgBr f a b : f @ F --> a -> f x - b @[x --> F] --> a - b.
+Proof. exact: cvgDr. 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 cvg0DC f a : f @ F --> 0 -> f x + a @[x --> F] --> a.
+Proof. by move=> /(cvgDr (b := a)); 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 cvgCD0 f a : f @ F --> 0 -> a + f x @[x --> F] --> a.
+Proof. by move/(@cvgDl _ a); 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 cvg0BC f a : f @ F --> 0 -> f x - a @[x --> F] --> -a.
+Proof. by move=> /(cvgBr (b := a)); 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 cvgCB0 f a : f @ F --> 0 -> a - f x @[x --> F] --> a.
+Proof. by move/(@cvgBl _ a); 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.

From 7607dd53424ebb74098d5e3299408d8f5e0a33c0 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 15:44:31 +0200
Subject: [PATCH 07/17] Update changelog

---
 CHANGELOG_UNRELEASED.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2d85fdc0a5..ee32fdf6d9 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -234,6 +234,13 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in file `normed_module.v`,
+  + new lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`, 
+    `cvgCM0`, and `cvgM0`.
+- in file `pseudometric_normed_Zmodule.v`,
+  + new lemmas `cvgDl`, `cvgDr`, `cvgBl`, `cvgBr`, `cvg0D`, `cvg0DC`, 
+    `cvgD0`, `cvgCD0`, `cvg0B`, `cvg0BC`, `cvgB0`, `cvgCB0`, and `cvgN0`.
+
 ### Changed
 
 - in `realsum.v`:

From 8e9b802ed4e8b363536bd083c3bf9d290cf379cf Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 13:53:44 +0200
Subject: [PATCH 08/17] Add dependency on #2029 for CI

---
 CHANGELOG_UNRELEASED.md                       |  7 ++++
 theories/normedtype_theory/normed_module.v    | 24 ++++++++++++
 .../pseudometric_normed_Zmodule.v             | 39 +++++++++++++++++++
 .../probability_theory/beta_distribution.v    |  1 -
 4 files changed, 70 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index e566816a2f..2ace5a393c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -234,6 +234,13 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in file `normed_module.v`,
+  + new lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`, 
+    `cvgCM0`, and `cvgM0`.
+- in file `pseudometric_normed_Zmodule.v`,
+  + new lemmas `cvgDl`, `cvgDr`, `cvgBl`, `cvgBr`, `cvg0D`, `cvg0DC`, 
+    `cvgD0`, `cvgCD0`, `cvg0B`, `cvg0BC`, `cvgB0`, `cvgCB0`, and `cvgN0`.
+
 - in `derive.v`
   + new lemmas `derive1Dn`, `der1_scaleLR`, `deriveZLR`, `derivableZLR`, 
     `derivable_shiftf`, `derive_shiftf`, `is_derive_shiftf`, `derive1_shiftf`, 
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 1252178b3f..94a72d0f8e 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -642,6 +642,30 @@ 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 cvg1MC f a : f @ F --> (1 :> K) -> f x * a @[x --> F] --> a.
+Proof. by move/(cvgMr_tmp (b := a)); rewrite mul1r. 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 cvgCM1 f a : f @ F --> (1 :> K) -> a * f x @[x --> F] --> a.
+Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr1. 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 cvg0MC f a : f @ F --> 0 -> f x * a @[x --> F] --> 0.
+Proof. by move/(cvgMr_tmp (b := a)); rewrite mul0r. 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 cvgCM0 f a : f @ F --> 0 -> a * f x @[x --> F] --> 0.
+Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr0. 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.
 
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 9f945624de..82c259cf1f 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -1098,6 +1098,45 @@ 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 cvgDl f a b : f @ F --> b -> a + f x @[x --> F] --> a + b.
+Proof. apply: cvgD; exact: cvg_cst. Qed.
+
+Lemma cvgDr f a b : f @ F --> a -> f x + b @[x --> F] --> a + b.
+Proof. move/cvgD; apply; exact: cvg_cst. Qed.
+
+Lemma cvgBl f a b : f @ F --> b -> a - f x @[x --> F] --> a - b.
+Proof. by move/cvgN; apply: cvgDl. Qed.
+
+Lemma cvgBr f a b : f @ F --> a -> f x - b @[x --> F] --> a - b.
+Proof. exact: cvgDr. 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 cvg0DC f a : f @ F --> 0 -> f x + a @[x --> F] --> a.
+Proof. by move=> /(cvgDr (b := a)); 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 cvgCD0 f a : f @ F --> 0 -> a + f x @[x --> F] --> a.
+Proof. by move/(@cvgDl _ a); 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 cvg0BC f a : f @ F --> 0 -> f x - a @[x --> F] --> -a.
+Proof. by move=> /(cvgBr (b := a)); 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 cvgCB0 f a : f @ F --> 0 -> a - f x @[x --> F] --> a.
+Proof. by move/(@cvgBl _ a); 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.
diff --git a/theories/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v
index 9a879b1443..832378557a 100644
--- a/theories/probability_theory/beta_distribution.v
+++ b/theories/probability_theory/beta_distribution.v
@@ -77,7 +77,6 @@ Lemma derive_onemXn n x :
   (fun y => y.~ ^+ n)^`()%classic x = - n%:R * x.~ ^+ n.-1.
 Proof.
 rewrite (@derive1_comp _ (@onem _) (fun x => x ^+ n))//.
-  exact: exprn_derivable.
 rewrite derive1E exp_derive// derive1E deriveB// -derive1E.
 by rewrite derive1_cst derive_id sub0r mulrN1 [in RHS]mulNr scaler1.
 Qed.

From 022fed0fa800fa0ec81f8e3482a46cbc34101507 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 14:03:30 +0200
Subject: [PATCH 09/17] Topology lemmas

---
 theories/topology_theory/function_spaces.v  |  5 ++
 theories/topology_theory/metric_structure.v | 27 -----------
 theories/topology_theory/nat_topology.v     | 12 +++++
 theories/topology_theory/num_topology.v     | 54 +++++++++++++++++++++
 4 files changed, 71 insertions(+), 27 deletions(-)

diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v
index 8c82e106d0..432d5a00bc 100644
--- a/theories/topology_theory/function_spaces.v
+++ b/theories/topology_theory/function_spaces.v
@@ -1600,6 +1600,11 @@ Proof.
 by move=> F_cont x; apply: cvg_big => // i /F_cont; exact.
 Qed.
 
+Lemma within_continuous_big (T : topologicalType) (A : set T) (r : seq I) (F : I -> T -> U) :
+	(forall (i : I), P i -> {within A, continuous (F i)}) ->
+	{within A, continuous (fun x : T => \big[op/x0]_(i <- r | P i) F i x)}.
+Proof. by move=> cont_F x; apply: continuous_big. Qed.
+
 End big_continuous.
 
 Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y :=
diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v
index d9477e84cb..34da60f8d8 100644
--- a/theories/topology_theory/metric_structure.v
+++ b/theories/topology_theory/metric_structure.v
@@ -315,33 +315,6 @@ Unshelve. all: end_near. Qed.
 
 End cvg_nbhsP.
 
-Section cvg_at_right_left_dnbhs.
-Variables (R : realFieldType) (T : metricType R).
-
-Import metricType_numDomainType.
-
-Lemma cvg_at_right_left_dnbhs (f : R -> T) (p : R) (l : T) :
-  f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l ->
-  f x @[x --> p^'] --> l.
-Proof.
-move=> /cvgrPdist_le fppl /cvgrPdist_le fpnl; apply/cvgrPdist_le => e e0.
-have {fppl}[a /= a0 fppl] := fppl (at_right_proper_filter p) _ e0.
-have {fpnl}[b /= b0 fpnl] := fpnl (at_left_proper_filter p) _ e0.
-near=> t.
-have : t != p by near: t; exact: nbhs_dnbhs_neq.
-rewrite neq_lt => /orP[tp|pt].
-- apply: fpnl => //=; near: t.
-  exists (b / 2) => //=; first by rewrite divr_gt0.
-  move=> z/= + _ => /lt_le_trans; apply.
-  by rewrite ler_pdivrMr// ler_pMr// ler1n.
-- apply: fppl =>//=; near: t.
-  exists (a / 2) => //=; first by rewrite divr_gt0.
-  move=> z/= + _ => /lt_le_trans; apply.
-  by rewrite ler_pdivrMr// ler_pMr// ler1n.
-Unshelve. all: by end_near. Qed.
-
-End cvg_at_right_left_dnbhs.
-
 Section at_left_rightR.
 Variable (R : numFieldType).
 
diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v
index e2d0274f38..49ae67d0ac 100644
--- a/theories/topology_theory/nat_topology.v
+++ b/theories/topology_theory/nat_topology.v
@@ -93,6 +93,18 @@ Lemma near_inftyS (P : set nat) :
   (\forall x \near \oo, P (S x)) -> (\forall x \near \oo, P x).
 Proof. case=> N _ NPS; exists (S N) => // [[]]; rewrite /= ?ltn0 //. Qed.
 
+Lemma near_infty_after (P : set nat) :
+  (\forall n \near \oo, P n) <-> (\forall N \near \oo, forall n, (n >= N)%N -> P n).
+Proof.
+split.
+- move=> [N _ afterN].
+  exists N => // n /= /[swap] n' /leq_trans /[apply].
+  exact: afterN.
+- move=> [N _ afterN].
+  exists N => // n /=.
+  by apply: afterN => /=.
+Qed.  
+
 Section infty_nat.
 Local Open Scope nat_scope.
 
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index fc7caea215..69e4cda5e5 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -241,6 +241,50 @@ split=> [pPf e|ex_notPx].
   by rewrite /ball/= ltr0_norm ?subr_lt0// opprB ltrBlDl.
 Unshelve. all: by end_near. Qed.
 
+Lemma at_rightD x a : (x + a)^'+ = (y + a @[y --> x^'+]).
+Proof.
+apply/seteqP; split=> P /=.
+- move=> [/= r r0 br_sub].
+  exists r => // y bxy x_lt_y.
+  apply: br_sub => /=.
+  + by rewrite (addrC y) addrKA.
+  + by rewrite ltrD2r.
+- move=> [/= r r0 br_sub].
+  exists r => // y bxay xDa_lt_y.
+  rewrite -(subrK a y).
+  apply: br_sub => /=.
+  + by rewrite opprB addrA.
+  + by rewrite ltrBrDr.
+Qed.
+
+Lemma at_leftD x a : (x + a)^'- = (y + a @[y --> x^'-]).
+Proof.
+apply/seteqP; split=> P /=.
+- move=> [/= r r0 br_sub].
+  exists r => // y bxy x_gt_y.
+  apply: br_sub => /=.
+  + by rewrite (addrC y) addrKA.
+  + by rewrite ltrD2r.
+- move=> [/= r r0 br_sub].
+  exists r => // y bxay xDa_gt_y.
+  rewrite -(subrK a y).
+  apply: br_sub => /=.
+  + by rewrite opprB addrA.
+  + by rewrite ltrBlDr.
+Qed.
+
+Lemma near_at_rightD x a (P : set R) : (\forall y \near (x + a)^'+, P y) = (\forall y \near x^'+, P (y + a)).
+Proof. by rewrite at_rightD near_map. Qed.
+
+Lemma near_at_leftD x a (P : set R) : (\forall y \near (x + a)^'-, P y) = (\forall y \near x^'-, P (y + a)).
+Proof. by rewrite at_leftD near_map. Qed.
+
+Lemma at_left_shift (T : Type) x a (f : R -> T) : (f @ (x + a)^'-) = (f (y + a) @[y --> x^'-]).
+Proof. by rewrite at_leftD. Qed.
+
+Lemma at_right_shift (T : Type) x a (f : R -> T) : (f @ (x + a)^'+) = (f (y + a) @[y --> x^'+]).
+Proof. by rewrite at_rightD. Qed.
+
 End at_left_right.
 #[global] Typeclasses Opaque at_left at_right.
 Notation "x ^'-" := (at_left x) : classical_set_scope.
@@ -252,6 +296,16 @@ Notation "x ^'+" := (at_right x) : classical_set_scope.
 #[global] Hint Extern 0 (Filter (nbhs _^'-)) =>
   (apply: at_left_proper_filter) : typeclass_instances.
 
+Lemma cvg_at_right_left_dnbhs (R : realFieldType) (T : topologicalType) (f : R -> T) (p : R) (l : T) :
+  f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l -> f x @[x --> p^'] --> l.
+Proof.
+move=> + + U Uz => /(_ U Uz) + /(_ U Uz); near_simpl.
+rewrite !near_withinE !near_nbhs => lf rf.
+apply: filter_app lf; apply: filter_app rf.
+near=> t => xlt xgt.
+by case/lt_total/orP.
+Unshelve. all: by end_near. Qed.
+
 Lemma left_right_continuousP {R : realFieldType} {T : topologicalType}
     (f : R -> T) x :
   f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x.

From fa30e1fb33a4e2a54292f7d88b98a05d697fe66d Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 16:10:48 +0200
Subject: [PATCH 10/17] normed module neighborhood lemmas

---
 theories/normedtype_theory/num_normedtype.v   | 86 +++++++++++++++++++
 .../pseudometric_normed_Zmodule.v             | 16 ++++
 theories/normedtype_theory/tvs.v              | 27 ++++++
 3 files changed, 129 insertions(+)

diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v
index 9457d67f93..9b8c182fd2 100644
--- a/theories/normedtype_theory/num_normedtype.v
+++ b/theories/normedtype_theory/num_normedtype.v
@@ -245,6 +245,53 @@ apply/seteqP; split => [A [M [Mreal MA]]|A [M [Mreal MA]]].
 by exists (- M); rewrite ?realN; split=> // x; rewrite ltrNl => /MA.
 Qed.
 
+Lemma pinftyV (R : numFieldType) : x^-1 @[x --> +oo] = (0 : R)^'+.
+Proof.
+apply/seteqP; split=> [A [M [Mreal MA]]|A [r /= r0 rA]].
+- have mM1_gt0 : 0 < Num.max M 1.
+    case: (@real_leP _ M 1) => //.
+    by apply: lt_trans.
+  exists (Num.max M 1)^-1; first by rewrite /= invr_gt0.
+  move=> x /= /[swap] x_gt0.
+  rewrite distrC subr0 gtr0_norm// invf_pgt ?posrE// => mM1_lt_xV.
+  rewrite -(invrK x); apply: MA.
+  apply: le_lt_trans mM1_lt_xV.
+  by case: (@real_leP _ M 1).
+- exists r^-1; split; first by rewrite realV gtr0_real.
+  move=> x /[dup] rV_lt_x.
+  have x_gt0 : x > 0.
+    apply: lt_trans rV_lt_x.
+    by rewrite invr_gt0.
+  rewrite invf_plt// => xV_lt_r.
+  apply: rA; last by rewrite invr_gt0.
+  by rewrite /= distrC subr0 gtr0_norm// invr_gt0.
+Qed.
+
+Lemma ninftyV (R : numFieldType) : x^-1 @[x --> -oo] = (0 : R)^'-.
+Proof.
+apply/seteqP; split=> [A [M [Mreal MA]]|A [r /= r0 rA]].
+- pose M' := Num.min M (-1).
+  have M'_lt0 : M' < 0.
+    rewrite /M'.
+    case: (@real_leP _ M (-1)) => // /le_lt_trans.
+    by apply.
+  exists (-M')^-1; first by rewrite /= invr_gt0 oppr_gt0.
+  move=> x /= /[swap] x_lt0.
+  rewrite distrC subr0 ltr0_norm// invrN ltrN2 => x_gt_VM'.
+  rewrite -(invrK x); apply: MA.
+  apply: (lt_le_trans (y := M')).
+  + by rewrite invf_nlt.
+  + by rewrite /M'; case: (@real_ltP _ M (-1)).
+- exists (- r^-1); split; first by rewrite realN realV gtr0_real.
+  move=> x /[dup] x_lt_NrV.
+  have x_lt0 : x < 0.
+    apply: (lt_trans x_lt_NrV).
+    by rewrite oppr_lt0 invr_gt0.
+  rewrite ltrNr invf_plt// ?posrE ?oppr_gt0// => NxV_lt_r.
+  apply: rA; last by rewrite invr_lt0.
+  by rewrite /= distrC subr0 ltr0_norm ?invr_lt0// -invrN.
+Qed.
+
 Section infty_nbhs_instances.
 Context {R : numFieldType}.
 Implicit Types r : R.
@@ -441,6 +488,20 @@ Unshelve. all: end_near. Qed.
 Lemma cvgNrNy f : (- f @ F --> -oo) <-> (f @ F --> +oo).
 Proof. by rewrite -cvgNry opprK. Qed.
 
+Lemma cvgryV f : f @ F --> +oo -> (f x)^-1 @[x --> F] --> (0 : R).
+Proof.
+move=> cvgy.
+apply: cvg_comp; first exact: cvgy.
+by rewrite pinftyV; exact: cvg_within.
+Qed.
+
+Lemma cvgrNyV f : f @ F --> -oo -> (f x)^-1 @[x --> F] --> (0 : R).
+Proof.
+move=> cvgNy.
+apply: cvg_comp; first exact: cvgNy.
+by rewrite ninftyV; exact: cvg_within.
+Qed.
+
 End cvg_infty_numField.
 
 Section cvg_infty_realField.
@@ -526,6 +587,31 @@ Proof. by move=> fy; under eq_fun do rewrite mulrC; exact: gt0_cvgMly. Qed.
 
 End gt0_cvg.
 
+Section lt0_cvg.
+Context {R : realFieldType} {F : set_system R} {FF : Filter F}.
+Variables (M : R) (f : R -> R).
+Hypothesis M0 : M < 0.
+
+Lemma lt0_cvgMlNy : (f r) @[r --> F] --> +oo -> (f r * M)%R @[r --> F] --> -oo.
+Proof.
+move=> /cvgryPge fy; apply/cvgrNyPle => A.
+by apply: filterS (fy (A / M)) => x; rewrite ler_ndivrMr.
+Qed.
+
+Lemma lt0_cvgMrNy : (f r) @[r --> F] --> +oo -> (M * f r)%R @[r --> F] --> -oo.
+Proof. by move=> fy; under eq_fun do rewrite mulrC; exact: lt0_cvgMlNy. Qed.
+
+Lemma lt0_cvgMly : f r @[r --> F] --> -oo -> (f r * M)%R @[r --> F] --> +oo.
+Proof.
+move=> /cvgrNyPle fNy; apply/cvgryPge => A.
+by apply: filterS (fNy (A / M)) => x; rewrite ler_ndivlMr.
+Qed.
+
+Lemma lt0_cvgMry : f r @[r --> F] --> -oo -> (M * f r)%R @[r --> F] --> +oo.
+Proof. by move=> fy; under eq_fun do rewrite mulrC; exact: lt0_cvgMly. Qed.
+
+End lt0_cvg.
+
 Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
     (l : set_system T) :
   f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l.
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 9f945624de..0add1a4aaf 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -628,6 +628,22 @@ Proof.
 by rewrite at_leftN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK.
 Qed.
 
+Lemma fmap_at_left0P {T : Type} {R : numFieldType} x (f : R -> T) : (f (x - e) @[e --> 0^'+]) = (f @ x^'-).
+Proof.
+rewrite -(subrr (-x)) at_right_shift at_rightN -fmap_comp.
+apply: near_eq_cvgE.
+apply: (nearW (F := x^'-)) => y /=.
+by rewrite opprB addNKr opprK.
+Qed.
+
+Lemma fmap_at_right0E {T : Type} {R : numFieldType} (x : R) (f : R -> T) : (f (x + e) @[e --> 0^'+]) = (f @ x^'+).
+Proof.
+rewrite -(subrr x) at_right_shift.
+apply: near_eq_cvgE.
+apply: (nearW (F := x^'+)) => y.
+by rewrite addrC subrK.
+Qed.
+
 Section at_left_right_pseudoMetricNormedZmod.
 Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R).
 
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 41126a781d..85b1a0a54c 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -647,6 +647,19 @@ Proof. exact/nbhsB_subproof/add_continuous. Qed.
 
 End ConvexTvs_numDomain.
 
+Lemma near_shiftE (R : numDomainType) (E : convexTvsType R) (U : set E) (x a : E) :
+  (\forall y \near x + a, U y) = (\near x, U (x + a)).
+Proof.
+eqProp; rewrite -!nbhs_nearE.
+- move/(nbhsB (-a)).
+  rewrite addrC addrK.
+  apply: filterS => _ [y Uy <-].
+  by rewrite addrC addNKr.
+- move/(nbhsB a); rewrite addrC.
+  apply: filterS => ? [y Uya <-].
+  by rewrite addrC.
+Qed.
+
 Section ConvexTvs_numField.
 
 Lemma nbhs0Z (R : numFieldType) (E : convexTvsType R) (U : set E) (r : R) :
@@ -667,6 +680,20 @@ near=> z; exists (r^-1 *: z); last by rewrite scalerA divff// scale1r.
 by apply: (BU (r^-1,z)); split; [exact: nbhs_singleton|near: z].
 Unshelve. all: by end_near. Qed.
 
+Lemma nearZE (R : numFieldType) (T : convexTvsType R) (c : R) (x : T) (P : set T) :
+  c != 0 -> (\forall y \near c *: x, P y) = (\near x, P (c *: x)).
+Proof.
+move=> c_neq0.
+have cinv_neq0 : c^-1 != 0 by apply: invr_neq0.
+eqProp.
+- move/(nbhsZ cinv_neq0).
+  rewrite scalerK//.
+  apply: filterS => ? [y Py <-].
+  by rewrite scalerKV.
+- move/(nbhsZ c_neq0).
+  by apply: filterS => ? [y Pcy <-].
+Qed.
+
 End ConvexTvs_numField.
 
 Section standard_topology.

From cbb96a16e8f1e9ee421f163a9cd8072e6359f5b8 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 16:11:35 +0200
Subject: [PATCH 11/17] Update changelog

---
 CHANGELOG_UNRELEASED.md | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9522855b6e..8f59828701 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -236,6 +236,22 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in file `function_spaces.v`,
+  + new lemma `within_continuous_big`.
+- in file `nat_topology.v`,
+  + new lemma `near_infty_after`.
+- in file `num_topology.v`,
+  + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, 
+    `at_left_shift`, and `at_right_shift`.
+
+- in file `num_normedtype.v`,
+  + new lemmas `pinftyV`, `ninftyV`, `cvgryV`, `cvgrNyV`, `lt0_cvgMlNy`, 
+    `lt0_cvgMrNy`, `lt0_cvgMly`, and `lt0_cvgMry`.
+- in file `pseudometric_normed_Zmodule.v`,
+  + new lemmas `fmap_at_left0P`, and `fmap_at_right0E`.
+- in file `tvs.v`,
+  + new lemmas `near_shiftE`, and `nearZE`.
+
 ### Changed
 
 - in `realsum.v`:
@@ -356,6 +372,9 @@
 - in `classical_sets.v`
   + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`)
 
+- moved from `metric_structure.v` to `num_topology.v`: 
+  + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`.
+
 ### Renamed
 
 - in `tvs.v`:

From 553bc3a46c381ccccaede8b2f6a9231a5a596907 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 14:03:30 +0200
Subject: [PATCH 12/17] Add dependency on #2027 for CI

---
 CHANGELOG_UNRELEASED.md                     | 10 ++++
 theories/topology_theory/function_spaces.v  |  5 ++
 theories/topology_theory/metric_structure.v | 27 -----------
 theories/topology_theory/nat_topology.v     | 12 +++++
 theories/topology_theory/num_topology.v     | 54 +++++++++++++++++++++
 5 files changed, 81 insertions(+), 27 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2ace5a393c..f646190c7a 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -234,6 +234,14 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in file `function_spaces.v`,
+  + new lemma `within_continuous_big`.
+- in file `nat_topology.v`,
+  + new lemma `near_infty_after`.
+- in file `num_topology.v`,
+  + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, 
+    `at_left_shift`, and `at_right_shift`.
+
 - in file `normed_module.v`,
   + new lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`, 
     `cvgCM0`, and `cvgM0`.
@@ -369,6 +377,8 @@
 
 - moved from `realfun.v` to `derive.v`: 
   + lemmas `is_deriveV`, `is_derive1_comp`.
+- moved from `metric_structure.v` to `num_topology.v`: 
+  + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`.
 
 ### Renamed
 
diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v
index 8c82e106d0..432d5a00bc 100644
--- a/theories/topology_theory/function_spaces.v
+++ b/theories/topology_theory/function_spaces.v
@@ -1600,6 +1600,11 @@ Proof.
 by move=> F_cont x; apply: cvg_big => // i /F_cont; exact.
 Qed.
 
+Lemma within_continuous_big (T : topologicalType) (A : set T) (r : seq I) (F : I -> T -> U) :
+	(forall (i : I), P i -> {within A, continuous (F i)}) ->
+	{within A, continuous (fun x : T => \big[op/x0]_(i <- r | P i) F i x)}.
+Proof. by move=> cont_F x; apply: continuous_big. Qed.
+
 End big_continuous.
 
 Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y :=
diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v
index d9477e84cb..34da60f8d8 100644
--- a/theories/topology_theory/metric_structure.v
+++ b/theories/topology_theory/metric_structure.v
@@ -315,33 +315,6 @@ Unshelve. all: end_near. Qed.
 
 End cvg_nbhsP.
 
-Section cvg_at_right_left_dnbhs.
-Variables (R : realFieldType) (T : metricType R).
-
-Import metricType_numDomainType.
-
-Lemma cvg_at_right_left_dnbhs (f : R -> T) (p : R) (l : T) :
-  f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l ->
-  f x @[x --> p^'] --> l.
-Proof.
-move=> /cvgrPdist_le fppl /cvgrPdist_le fpnl; apply/cvgrPdist_le => e e0.
-have {fppl}[a /= a0 fppl] := fppl (at_right_proper_filter p) _ e0.
-have {fpnl}[b /= b0 fpnl] := fpnl (at_left_proper_filter p) _ e0.
-near=> t.
-have : t != p by near: t; exact: nbhs_dnbhs_neq.
-rewrite neq_lt => /orP[tp|pt].
-- apply: fpnl => //=; near: t.
-  exists (b / 2) => //=; first by rewrite divr_gt0.
-  move=> z/= + _ => /lt_le_trans; apply.
-  by rewrite ler_pdivrMr// ler_pMr// ler1n.
-- apply: fppl =>//=; near: t.
-  exists (a / 2) => //=; first by rewrite divr_gt0.
-  move=> z/= + _ => /lt_le_trans; apply.
-  by rewrite ler_pdivrMr// ler_pMr// ler1n.
-Unshelve. all: by end_near. Qed.
-
-End cvg_at_right_left_dnbhs.
-
 Section at_left_rightR.
 Variable (R : numFieldType).
 
diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v
index e2d0274f38..49ae67d0ac 100644
--- a/theories/topology_theory/nat_topology.v
+++ b/theories/topology_theory/nat_topology.v
@@ -93,6 +93,18 @@ Lemma near_inftyS (P : set nat) :
   (\forall x \near \oo, P (S x)) -> (\forall x \near \oo, P x).
 Proof. case=> N _ NPS; exists (S N) => // [[]]; rewrite /= ?ltn0 //. Qed.
 
+Lemma near_infty_after (P : set nat) :
+  (\forall n \near \oo, P n) <-> (\forall N \near \oo, forall n, (n >= N)%N -> P n).
+Proof.
+split.
+- move=> [N _ afterN].
+  exists N => // n /= /[swap] n' /leq_trans /[apply].
+  exact: afterN.
+- move=> [N _ afterN].
+  exists N => // n /=.
+  by apply: afterN => /=.
+Qed.  
+
 Section infty_nat.
 Local Open Scope nat_scope.
 
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index fc7caea215..69e4cda5e5 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -241,6 +241,50 @@ split=> [pPf e|ex_notPx].
   by rewrite /ball/= ltr0_norm ?subr_lt0// opprB ltrBlDl.
 Unshelve. all: by end_near. Qed.
 
+Lemma at_rightD x a : (x + a)^'+ = (y + a @[y --> x^'+]).
+Proof.
+apply/seteqP; split=> P /=.
+- move=> [/= r r0 br_sub].
+  exists r => // y bxy x_lt_y.
+  apply: br_sub => /=.
+  + by rewrite (addrC y) addrKA.
+  + by rewrite ltrD2r.
+- move=> [/= r r0 br_sub].
+  exists r => // y bxay xDa_lt_y.
+  rewrite -(subrK a y).
+  apply: br_sub => /=.
+  + by rewrite opprB addrA.
+  + by rewrite ltrBrDr.
+Qed.
+
+Lemma at_leftD x a : (x + a)^'- = (y + a @[y --> x^'-]).
+Proof.
+apply/seteqP; split=> P /=.
+- move=> [/= r r0 br_sub].
+  exists r => // y bxy x_gt_y.
+  apply: br_sub => /=.
+  + by rewrite (addrC y) addrKA.
+  + by rewrite ltrD2r.
+- move=> [/= r r0 br_sub].
+  exists r => // y bxay xDa_gt_y.
+  rewrite -(subrK a y).
+  apply: br_sub => /=.
+  + by rewrite opprB addrA.
+  + by rewrite ltrBlDr.
+Qed.
+
+Lemma near_at_rightD x a (P : set R) : (\forall y \near (x + a)^'+, P y) = (\forall y \near x^'+, P (y + a)).
+Proof. by rewrite at_rightD near_map. Qed.
+
+Lemma near_at_leftD x a (P : set R) : (\forall y \near (x + a)^'-, P y) = (\forall y \near x^'-, P (y + a)).
+Proof. by rewrite at_leftD near_map. Qed.
+
+Lemma at_left_shift (T : Type) x a (f : R -> T) : (f @ (x + a)^'-) = (f (y + a) @[y --> x^'-]).
+Proof. by rewrite at_leftD. Qed.
+
+Lemma at_right_shift (T : Type) x a (f : R -> T) : (f @ (x + a)^'+) = (f (y + a) @[y --> x^'+]).
+Proof. by rewrite at_rightD. Qed.
+
 End at_left_right.
 #[global] Typeclasses Opaque at_left at_right.
 Notation "x ^'-" := (at_left x) : classical_set_scope.
@@ -252,6 +296,16 @@ Notation "x ^'+" := (at_right x) : classical_set_scope.
 #[global] Hint Extern 0 (Filter (nbhs _^'-)) =>
   (apply: at_left_proper_filter) : typeclass_instances.
 
+Lemma cvg_at_right_left_dnbhs (R : realFieldType) (T : topologicalType) (f : R -> T) (p : R) (l : T) :
+  f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l -> f x @[x --> p^'] --> l.
+Proof.
+move=> + + U Uz => /(_ U Uz) + /(_ U Uz); near_simpl.
+rewrite !near_withinE !near_nbhs => lf rf.
+apply: filter_app lf; apply: filter_app rf.
+near=> t => xlt xgt.
+by case/lt_total/orP.
+Unshelve. all: by end_near. Qed.
+
 Lemma left_right_continuousP {R : realFieldType} {T : topologicalType}
     (f : R -> T) x :
   f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x.

From 49b25e079dc8bffce346e5d119bf6c7f261004a8 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 17:02:17 +0200
Subject: [PATCH 13/17] Correct dependency to #2024

---
 CHANGELOG_UNRELEASED.md                     | 12 +----
 classical/filter.v                          | 52 ++++++++++++++++++++
 theories/topology_theory/function_spaces.v  |  5 --
 theories/topology_theory/metric_structure.v | 27 +++++++++++
 theories/topology_theory/nat_topology.v     | 12 -----
 theories/topology_theory/num_topology.v     | 54 ---------------------
 6 files changed, 81 insertions(+), 81 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f646190c7a..97af2be1c7 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -126,6 +126,8 @@
 
 - in `filter.v`:
   + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType`
+  + new lemmas `near_eq_cvgE`, `near_eq_is_cvg`, `near_eq_lim`, 
+    `cvg_to_eq`, `cvg_to_withinP`, and `within_cvg_to_within`.
 
 - in `topology_structure.v`:
   + structure `SubTopological`, notation `subTopologicalType`
@@ -234,14 +236,6 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
-- in file `function_spaces.v`,
-  + new lemma `within_continuous_big`.
-- in file `nat_topology.v`,
-  + new lemma `near_infty_after`.
-- in file `num_topology.v`,
-  + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, 
-    `at_left_shift`, and `at_right_shift`.
-
 - in file `normed_module.v`,
   + new lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`, 
     `cvgCM0`, and `cvgM0`.
@@ -377,8 +371,6 @@
 
 - moved from `realfun.v` to `derive.v`: 
   + lemmas `is_deriveV`, `is_derive1_comp`.
-- moved from `metric_structure.v` to `num_topology.v`: 
-  + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`.
 
 ### Renamed
 
diff --git a/classical/filter.v b/classical/filter.v
index b26d00d72f..4233a6d9bc 100644
--- a/classical/filter.v
+++ b/classical/filter.v
@@ -925,10 +925,23 @@ Lemma near_eq_cvg {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) :
   {near F, f =1 g} -> g @ F `=>` f @ F.
 Proof. by move=> eq_fg P /=; apply: filterS2 eq_fg => x /= <-. Qed.
 
+Lemma near_eq_cvgE {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) :
+  {near F, f =1 g} -> f @ F = g @ F.
+Proof.
+move=> eq_fg.
+apply/seteqP; split; apply: near_eq_cvg => //.
+by near do symmetry.
+Unshelve. all: by end_near.
+Qed.
+
 Lemma eq_cvg (T T' : Type) (F : set_system T) (f g : T -> T') (x : set_system T') :
   f =1 g -> (f @ F --> x) = (g @ F --> x).
 Proof. by move=> /funext->. Qed.
 
+Lemma near_eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') : 
+  Filter F -> {near F, g =1 f} -> cvg (f x @[x --> F]) -> cvg(g x @[x --> F]).
+Proof. by move=> /@near_eq_cvgE /[apply] ->. Qed.
+
 Lemma eq_is_cvg_in (T T' : Type) (fT : pfilteredType T') (F : set_system T) (f g : T -> T') :
   f =1 g -> [cvg (f @ F) in fT] = [cvg (g @ F) in fT].
 Proof. by move=> /funext->. Qed.
@@ -937,6 +950,14 @@ Lemma eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') :
   f =1 g -> cvg (f @ F) = cvg (g @ F).
 Proof. by move=> /funext->. Qed.
 
+Lemma near_eq_lim (T : Type) (T' : pnbhsType) {F : set_system T} {FF : Filter F} (f g : T -> T') :
+  {near F, f =1 g} -> lim (f @ F) = lim (g @ F).
+Proof. by move=> /near_eq_cvgE ->. Qed.
+
+Lemma cvg_to_eq {T : nbhsType} {F : set_system T} (l l' : T) :
+  F --> l' -> l = l' -> F --> l.
+Proof. by move=> + ->. Qed.
+
 Lemma neari_eq_loc {T U} {F : set_system T} {FF : Filter F} (f g : T -> set U) :
   {near F, f =2 g} -> g `@ F `=>` f `@ F.
 Proof.
@@ -1197,6 +1218,25 @@ Qed.
 
 End within.
 
+Lemma cvg_to_withinP (T U : Type) {F : set_system T} {FF : Filter F} {G : set_system U} {FG : Filter G} 
+    (f : T -> U) (A : set U) :
+  (f @ F --> within A G) <-> (f @ F --> G /\ \forall x \near F, A (f x)).
+Proof.
+split.
+  move=> cvg_w; split.
+  - apply: (cvg_trans cvg_w).
+    exact: cvg_within.
+  - apply: cvg_w.
+    exact: withinT.
+move=> [cvgT nearfA] P. 
+rewrite !nbhs_nearE near_withinE.
+move: cvgT => /[apply].
+rewrite near_map appfilter nbhs_nearE => nearF_AP.
+near=> x.
+suff : A (f x) by near: x.
+by near: x.
+Unshelve. all: by end_near. Qed.
+
 Global Instance within_filter T D F : Filter F -> Filter (@within T D F).
 Proof.
 move=> FF; rewrite /within; constructor => /=.
@@ -1210,6 +1250,18 @@ Qed.
 Canonical within_filter_on T D (F : filter_on T) :=
   FilterType (within D F) (within_filter _ _).
 
+Lemma within_cvg_to_within (T U : Type) {F : set_system T} {FF : Filter F} {G : set_system U} {FG : Filter G}
+    (f : T -> U) (A : set T) (B : set U) :
+  (\forall x \near F, A x -> B (f x)) -> f @ F --> G -> f @ within A F --> within B G.
+Proof.
+move=> near_hom cvgT.
+apply/cvg_to_withinP; split.
+- apply: cvg_trans cvgT.
+  apply: cvg_app.
+  exact: cvg_within.
+- by rewrite near_withinE.
+Qed. 
+
 Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T)
   (F : set_system T) (P : set T) :
   Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) ->
diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v
index 432d5a00bc..8c82e106d0 100644
--- a/theories/topology_theory/function_spaces.v
+++ b/theories/topology_theory/function_spaces.v
@@ -1600,11 +1600,6 @@ Proof.
 by move=> F_cont x; apply: cvg_big => // i /F_cont; exact.
 Qed.
 
-Lemma within_continuous_big (T : topologicalType) (A : set T) (r : seq I) (F : I -> T -> U) :
-	(forall (i : I), P i -> {within A, continuous (F i)}) ->
-	{within A, continuous (fun x : T => \big[op/x0]_(i <- r | P i) F i x)}.
-Proof. by move=> cont_F x; apply: continuous_big. Qed.
-
 End big_continuous.
 
 Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y :=
diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v
index 34da60f8d8..d9477e84cb 100644
--- a/theories/topology_theory/metric_structure.v
+++ b/theories/topology_theory/metric_structure.v
@@ -315,6 +315,33 @@ Unshelve. all: end_near. Qed.
 
 End cvg_nbhsP.
 
+Section cvg_at_right_left_dnbhs.
+Variables (R : realFieldType) (T : metricType R).
+
+Import metricType_numDomainType.
+
+Lemma cvg_at_right_left_dnbhs (f : R -> T) (p : R) (l : T) :
+  f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l ->
+  f x @[x --> p^'] --> l.
+Proof.
+move=> /cvgrPdist_le fppl /cvgrPdist_le fpnl; apply/cvgrPdist_le => e e0.
+have {fppl}[a /= a0 fppl] := fppl (at_right_proper_filter p) _ e0.
+have {fpnl}[b /= b0 fpnl] := fpnl (at_left_proper_filter p) _ e0.
+near=> t.
+have : t != p by near: t; exact: nbhs_dnbhs_neq.
+rewrite neq_lt => /orP[tp|pt].
+- apply: fpnl => //=; near: t.
+  exists (b / 2) => //=; first by rewrite divr_gt0.
+  move=> z/= + _ => /lt_le_trans; apply.
+  by rewrite ler_pdivrMr// ler_pMr// ler1n.
+- apply: fppl =>//=; near: t.
+  exists (a / 2) => //=; first by rewrite divr_gt0.
+  move=> z/= + _ => /lt_le_trans; apply.
+  by rewrite ler_pdivrMr// ler_pMr// ler1n.
+Unshelve. all: by end_near. Qed.
+
+End cvg_at_right_left_dnbhs.
+
 Section at_left_rightR.
 Variable (R : numFieldType).
 
diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v
index 49ae67d0ac..e2d0274f38 100644
--- a/theories/topology_theory/nat_topology.v
+++ b/theories/topology_theory/nat_topology.v
@@ -93,18 +93,6 @@ Lemma near_inftyS (P : set nat) :
   (\forall x \near \oo, P (S x)) -> (\forall x \near \oo, P x).
 Proof. case=> N _ NPS; exists (S N) => // [[]]; rewrite /= ?ltn0 //. Qed.
 
-Lemma near_infty_after (P : set nat) :
-  (\forall n \near \oo, P n) <-> (\forall N \near \oo, forall n, (n >= N)%N -> P n).
-Proof.
-split.
-- move=> [N _ afterN].
-  exists N => // n /= /[swap] n' /leq_trans /[apply].
-  exact: afterN.
-- move=> [N _ afterN].
-  exists N => // n /=.
-  by apply: afterN => /=.
-Qed.  
-
 Section infty_nat.
 Local Open Scope nat_scope.
 
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index 69e4cda5e5..fc7caea215 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -241,50 +241,6 @@ split=> [pPf e|ex_notPx].
   by rewrite /ball/= ltr0_norm ?subr_lt0// opprB ltrBlDl.
 Unshelve. all: by end_near. Qed.
 
-Lemma at_rightD x a : (x + a)^'+ = (y + a @[y --> x^'+]).
-Proof.
-apply/seteqP; split=> P /=.
-- move=> [/= r r0 br_sub].
-  exists r => // y bxy x_lt_y.
-  apply: br_sub => /=.
-  + by rewrite (addrC y) addrKA.
-  + by rewrite ltrD2r.
-- move=> [/= r r0 br_sub].
-  exists r => // y bxay xDa_lt_y.
-  rewrite -(subrK a y).
-  apply: br_sub => /=.
-  + by rewrite opprB addrA.
-  + by rewrite ltrBrDr.
-Qed.
-
-Lemma at_leftD x a : (x + a)^'- = (y + a @[y --> x^'-]).
-Proof.
-apply/seteqP; split=> P /=.
-- move=> [/= r r0 br_sub].
-  exists r => // y bxy x_gt_y.
-  apply: br_sub => /=.
-  + by rewrite (addrC y) addrKA.
-  + by rewrite ltrD2r.
-- move=> [/= r r0 br_sub].
-  exists r => // y bxay xDa_gt_y.
-  rewrite -(subrK a y).
-  apply: br_sub => /=.
-  + by rewrite opprB addrA.
-  + by rewrite ltrBlDr.
-Qed.
-
-Lemma near_at_rightD x a (P : set R) : (\forall y \near (x + a)^'+, P y) = (\forall y \near x^'+, P (y + a)).
-Proof. by rewrite at_rightD near_map. Qed.
-
-Lemma near_at_leftD x a (P : set R) : (\forall y \near (x + a)^'-, P y) = (\forall y \near x^'-, P (y + a)).
-Proof. by rewrite at_leftD near_map. Qed.
-
-Lemma at_left_shift (T : Type) x a (f : R -> T) : (f @ (x + a)^'-) = (f (y + a) @[y --> x^'-]).
-Proof. by rewrite at_leftD. Qed.
-
-Lemma at_right_shift (T : Type) x a (f : R -> T) : (f @ (x + a)^'+) = (f (y + a) @[y --> x^'+]).
-Proof. by rewrite at_rightD. Qed.
-
 End at_left_right.
 #[global] Typeclasses Opaque at_left at_right.
 Notation "x ^'-" := (at_left x) : classical_set_scope.
@@ -296,16 +252,6 @@ Notation "x ^'+" := (at_right x) : classical_set_scope.
 #[global] Hint Extern 0 (Filter (nbhs _^'-)) =>
   (apply: at_left_proper_filter) : typeclass_instances.
 
-Lemma cvg_at_right_left_dnbhs (R : realFieldType) (T : topologicalType) (f : R -> T) (p : R) (l : T) :
-  f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l -> f x @[x --> p^'] --> l.
-Proof.
-move=> + + U Uz => /(_ U Uz) + /(_ U Uz); near_simpl.
-rewrite !near_withinE !near_nbhs => lf rf.
-apply: filter_app lf; apply: filter_app rf.
-near=> t => xlt xgt.
-by case/lt_total/orP.
-Unshelve. all: by end_near. Qed.
-
 Lemma left_right_continuousP {R : realFieldType} {T : topologicalType}
     (f : R -> T) x :
   f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x.

From db98ac7940bcb9653eca56efc6815259bc4e229b Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 17:31:49 +0200
Subject: [PATCH 14/17] Missing `num_topology` lemmas

---
 CHANGELOG_UNRELEASED.md                 |  2 +-
 theories/topology_theory/num_topology.v | 40 +++++++++++++++++++++++++
 2 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 8f59828701..f1a493d980 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -242,7 +242,7 @@
   + new lemma `near_infty_after`.
 - in file `num_topology.v`,
   + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, 
-    `at_left_shift`, and `at_right_shift`.
+    `at_left_shift`, `at_right_shift`, `near_right_in_itv`, and `near_left_in_itv`.
 
 - in file `num_normedtype.v`,
   + new lemmas `pinftyV`, `ninftyV`, `cvgryV`, `cvgrNyV`, `lt0_cvgMlNy`, 
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index 69e4cda5e5..9e46a719b7 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -474,6 +474,46 @@ move=> r/=; rewrite ltr_pdivlMr// -ltrBlDr; apply: le_lt_trans.
 by rewrite -lerBlDr opprK addrC (le_trans (ler_norm _))// ler_peMr// ler1n.
 Qed.
 
+Lemma near_right_in_itv (R : realFieldType) (a : R) (P : set R) : 
+  (\forall b \near a^'+, {in `]a, b[, forall x, P x}) 
+  <-> {near a^'+, forall x, P x}.
+Proof.
+split=> [[/= r r0 hr]|[/= r r0 hr]].
+- exists (r / 2) => [|x /= /ltr_distlCDr x_lt_aDr2 a_lt_x].
+    by apply: divr_gt0.
+  apply: (hr (a + r / 2)) => /=.
+  + rewrite opprD addNKr normrN gtr0_norm// ?divr_gt0//.
+    by rewrite gtr_pMr// invf_plt ?posrE// invr1 ltrDl.
+  + by rewrite ltrDl divr_gt0.
+  + by rewrite in_itv/= a_lt_x/=.
+- exists r => // x /= /ltr_distlCDr x_lt_aDr a_lt_x y.
+  rewrite in_itv/= => /andP[a_lt_y y_lt_x].
+  apply: hr => //=.
+  rewrite distrC gtr0_norm ?subr_gt0// ltrBlDl.
+  by apply: lt_trans x_lt_aDr.
+Qed.
+
+Lemma near_left_in_itv (R : realFieldType) (b : R) (P : set R) : 
+  (\forall a \near b^'-, {in `]a, b[, forall x, P x}) 
+  <-> {near b^'-, forall x, P x}.
+Proof.
+split=> [[/= r r0 hr]|[/= r r0 hr]].
+- exists (r / 2) => [|x /= /ltr_distlDr b_lt_xDr2 x_lt_b].
+    by apply: divr_gt0.
+  apply: (hr (b - r / 2)) => /=.
+  + rewrite subKr gtr0_norm ?divr_gt0//.
+    by rewrite gtr_pMr// invf_plt ?posrE// invr1 ltrDl.
+  + by rewrite gtrBl divr_gt0.
+  + by rewrite in_itv/= x_lt_b andbT ltrBlDr.
+- exists r => // x /= /ltr_distlDr b_lt_xDr x_lt_b y.
+  rewrite in_itv/= => /andP[x_lt_y y_lt_b].
+  apply: hr => //=.
+  rewrite gtr0_norm ?subr_gt0//.
+  rewrite ltrBlDl.
+  apply: (lt_trans b_lt_xDr).
+  by rewrite ltrD2r.
+Qed.
+
 Section nbhs_lt_le.
 Context {R : numFieldType}.
 Implicit Types x z : R.

From 3862db44927d70d48046b8852815510a16d58d96 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 17:35:23 +0200
Subject: [PATCH 15/17] =?UTF-8?q?L'H=C3=B4pital's=20rule=20for=20infty/inf?=
 =?UTF-8?q?ty=20forms?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/realfun.v | 162 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 162 insertions(+)

diff --git a/theories/realfun.v b/theories/realfun.v
index dd0e368af8..6ba315aab4 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -2933,3 +2933,165 @@ move=> fgcl; apply/(@cvg_at_right_left_dnbhs _ R^o).
 Qed.
 
 End lhopital.
+
+Section lhopital_pinfty_at_right.
+Context (R : realType) (f df g dg : R -> R) (a l : R).
+Hypothesis near_der_f : \forall x \near a^'+, is_derive x (1 :> R) f (df x).
+Hypothesis near_der_g : \forall x \near a^'+, is_derive x (1 :> R) g (dg x).
+Hypothesis g_cvgy : g @ a^'+ --> +oo.
+Hypothesis near_dg_neq0 : (\forall x \near a^'+, dg x != 0).
+Hypothesis dfdg_cvg : df x / dg x @[x --> a^'+] --> l.
+
+Lemma lhopital_pinfty_at_right : f x / g x @[x --> a^'+] --> l.
+Proof.
+have [b a_lt_b in_ab] : exists2 b : R, a < b & 
+      {in `]a, b[%R, forall (x : R), [/\ 
+      is_derive x 1 f (df x) , 
+      is_derive x 1 g (dg x) &
+      dg x != 0
+    ]}.
+  near a^'+ => b.
+  exists b => //.
+  near: b; apply/near_right_in_itv.
+  by near do split.
+apply/cvgrPdistC_lt => /= eps eps0.
+near (0 :> R)^'+ => d.
+move: dfdg_cvg => /cvgrPdistC_lt /(_ d) [] //=.
+move=> r r0 withinr_withind.
+near a^'+ => y; near=> x.
+have := @cauchy_MVT R f df g dg x y.
+have /[swap] /[apply] : x < y by done.
+have /[swap] /[apply] : {within `[x, y], continuous f}.
+  apply: (continuous_subspaceW (B := `]a, b[)).
+    by apply: subset_itv; rewrite bnd_simp.
+  rewrite continuous_open_subspace// => /= z /set_mem/= z_ab.
+  apply: differentiable_continuous.
+  apply/derivable1_diffP.
+  apply: ex_derive.
+  by apply in_ab.
+have /[swap] /[apply] : {within `[x, y], continuous g}.
+  apply: (continuous_subspaceW (B := `]a, b[)).
+    by apply: subset_itv; rewrite bnd_simp.
+  rewrite continuous_open_subspace// => /= z /set_mem/= z_ab.
+  apply: differentiable_continuous.
+  apply/derivable1_diffP.
+  apply: ex_derive.
+  by apply in_ab.
+have xy_and z : z \in `]x, y[%R -> 
+    [/\ is_derive z 1 f (df z), is_derive z 1 g (dg z) & dg z != 0].
+  rewrite in_itv/= => /andP[x_lt_z z_lt_y].
+  apply: in_ab.
+  rewrite in_itv/=.
+  apply/andP; split.
+  - by apply: lt_trans x_lt_z.
+  - by apply: (lt_trans z_lt_y).
+move=> /(_ (fun z z_xy => let (h, _, _) := xy_and z z_xy in h)).
+move=> /(_ (fun z z_xy => let (_, h, _) := xy_and z z_xy in h)).
+move=> /(_ (fun z z_xy => let (_, _, h) := xy_and z z_xy in h)).
+clear xy_and in_ab.
+move=> [c + +].
+rewrite in_itv/= => /andP[x_lt_c c_lt_y] dfdgc.
+have : `|(f y - f x) / (g y - g x) - l| < d.
+  rewrite -dfdgc.
+  have a_lt_c : a < c by apply: (lt_trans (y := x)).
+  apply: withinr_withind => //=.
+  rewrite ltr0_norm ?subr_lt0// opprB ltrBlDl.
+  apply: (lt_trans c_lt_y).
+  near: y.
+  apply: nbhs_right_lt.
+  by rewrite ltrDl.
+have gx_gt_gy : g x > g y.
+  near: x.
+  by apply: cvgry_gt.
+have gx_gt0 : 0 < g x.
+  near: x.
+  by apply: cvgry_gt.
+have -> : (f y - f x) / (g y - g x) = (f x / g x - f y / g x) / (1 - g y / g x).
+  rewrite -[LHS]divrNN !opprB.
+  rewrite -(@divrr _ (g x)) ?unitf_gt0// -!mulrBl.
+  by rewrite -mulf_div divrr ?unitrV ?unitf_gt0// mulr1.
+rewrite ltr_distl ltr_pdivlMr.
+  by rewrite subr_gt0 ltr_pdivrMr// mul1r.
+rewrite ltrBrDr ltr_pdivrMr.
+  by rewrite subr_gt0 ltr_pdivrMr// mul1r.
+rewrite ltrBlDr => /andP[fg_gt fg_lt].
+rewrite ltr_distl.
+apply/andP; split.
+- apply: lt_trans fg_gt.
+  near: x.
+  apply: (cvgr_gt (l - d)); last first.
+    rewrite ltrD2l ltrN2.
+    near: d.
+    by apply: nbhs_right_lt.
+  apply: cvgD0.
+  + apply: cvgCM1.
+    apply: cvgCB0.
+    apply: cvgCM0.
+    by apply: cvgryV.
+  + apply: cvgCM0.
+    by apply: cvgryV.
+- apply: (lt_trans fg_lt).
+  near: x.
+  apply: (cvgr_lt (l + d)); last first.
+    rewrite ltrD2l.
+    near: d.
+    by apply: nbhs_right_lt.
+  apply: cvgD0.
+  + apply: cvgCM1.
+    apply: cvgCB0.
+    apply: cvgCM0.
+    by apply: cvgryV.
+  + apply: cvgCM0.
+    by apply: cvgryV.
+Unshelve. all: by end_near. Qed.
+
+End lhopital_pinfty_at_right.
+
+Section lhopital_pinfty_at_pinfty.
+Context (R : realType) (f df g dg : R -> R) (a l : R).
+Hypothesis near_der_f : \forall x \near +oo, is_derive x (1 :> R) f (df x).
+Hypothesis near_der_g : \forall x \near +oo, is_derive x (1 :> R) g (dg x).
+Hypothesis g_cvgy : g @ +oo --> +oo.
+Hypothesis near_dg_neq0 : (\forall x \near +oo, dg x != 0).
+Hypothesis dfdg_cvg : df x / dg x @[x --> +oo] --> l.
+
+Lemma lhopital_pinfty_at_pinfty : f x / g x @[x --> +oo] --> l.
+Proof.
+apply: cvg_trans.
+  apply: (near_eq_cvg (f := fun x => f x^-1^-1 / g x^-1^-1)).
+  by near=> x; rewrite !invrK.
+apply: (cvg_comp _ (fun x => f x^-1 / g x^-1)); first by rewrite pinftyV.
+apply: lhopital_pinfty_at_right.
+- near=> x.
+  apply: (is_derive1_comp (a := df x^-1)).
+    near: x.
+    rewrite -pinftyV near_map.
+    by near do rewrite invrK.
+  by apply: is_deriveV.
+- near=> x.
+  apply: (is_derive1_comp (a := dg x^-1)).
+    near: x.
+    rewrite -pinftyV near_map.
+    by near do rewrite invrK.
+  by apply: is_deriveV.
+- apply: cvg_comp => //.
+  apply: cvg_trans g_cvgy.
+  apply: cvg_fmap2.
+  rewrite -pinftyV -fmap_comp /comp.
+  by under eq_cvg do rewrite invrK.
+- near=> x.
+  rewrite scaler1 mulrN oppr_eq0.
+  apply: mulf_neq0.
+  + near: x.
+    rewrite -pinftyV near_map.
+    by near do rewrite invrK.
+  + by rewrite invr_neq0// sqrf_eq0.
+- apply: cvg_trans dfdg_cvg.
+  rewrite -pinftyV -fmap_comp.
+  apply: near_eq_cvg.
+  near=> x => /=.
+  rewrite !invrK scaler1 !(mulrN, divrN, mulNr) opprK -mulf_div divrr ?mulr1//.
+  by rewrite unitrV unitrX// unitrV unitf_gt0.
+Unshelve. all: by end_near. Qed.
+
+End lhopital_pinfty_at_pinfty.

From efaa663488d98d904b2b35fa8278ac835ff93e05 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 17:40:47 +0200
Subject: [PATCH 16/17] Update changelog

---
 CHANGELOG_UNRELEASED.md | 4 ++++
 theories/realfun.v      | 3 +--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f1a493d980..d0144463ca 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -252,6 +252,10 @@
 - in file `tvs.v`,
   + new lemmas `near_shiftE`, and `nearZE`.
 
+- in file `realfun.v`,
+  + new lemmas `lhopital_pinfty_at_right`, and 
+    `lhopital_pinfty_at_pinfty`.
+
 ### Changed
 
 - in `realsum.v`:
diff --git a/theories/realfun.v b/theories/realfun.v
index 6ba315aab4..b795e7a8c2 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -2965,8 +2965,7 @@ have /[swap] /[apply] : {within `[x, y], continuous f}.
   apply: (continuous_subspaceW (B := `]a, b[)).
     by apply: subset_itv; rewrite bnd_simp.
   rewrite continuous_open_subspace// => /= z /set_mem/= z_ab.
-  apply: differentiable_continuous.
-  apply/derivable1_diffP.
+  apply: differentiable_continuous; apply/derivable1_diffP.
   apply: ex_derive.
   by apply in_ab.
 have /[swap] /[apply] : {within `[x, y], continuous g}.

From 883e6b7c6b2b486487b98da237954d6452a607b0 Mon Sep 17 00:00:00 2001
From: Arthur Molina-Mounier <arthur.molina--mounier@ens.psl.eu>
Date: Wed, 15 Jul 2026 18:09:14 +0200
Subject: [PATCH 17/17] exponential growth lemmas

---
 CHANGELOG_UNRELEASED.md |  29 +++++----
 theories/exp.v          | 129 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 145 insertions(+), 13 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 1f15ac7553..62bbe28854 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -236,18 +236,6 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
-- in file `normed_module.v`,
-  + new lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`, 
-    `cvgCM0`, and `cvgM0`.
-- in file `pseudometric_normed_Zmodule.v`,
-  + new lemmas `cvgDl`, `cvgDr`, `cvgBl`, `cvgBr`, `cvg0D`, `cvg0DC`, 
-    `cvgD0`, `cvgCD0`, `cvg0B`, `cvg0BC`, `cvgB0`, `cvgCB0`, and `cvgN0`.
-
-- in `derive.v`
-  + new lemmas `derive1Dn`, `der1_scaleLR`, `deriveZLR`, `derivableZLR`, 
-    `derivable_shiftf`, `derive_shiftf`, `is_derive_shiftf`, `derive1_shiftf`, 
-    `near_eq_derive1n_near`, `near_eq_derive1_near`, `near_eq_derive1n`, and 
-    `near_eq_derive1`.
 - in file `function_spaces.v`,
   + new lemma `within_continuous_big`.
 - in file `nat_topology.v`,
@@ -256,14 +244,29 @@
   + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, 
     `at_left_shift`, `at_right_shift`, `near_right_in_itv`, and `near_left_in_itv`.
 
+- in file `normed_module.v`,
+  + new lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`, 
+    `cvgCM0`, and `cvgM0`.
 - in file `num_normedtype.v`,
   + new lemmas `pinftyV`, `ninftyV`, `cvgryV`, `cvgrNyV`, `lt0_cvgMlNy`, 
     `lt0_cvgMrNy`, `lt0_cvgMly`, and `lt0_cvgMry`.
 - in file `pseudometric_normed_Zmodule.v`,
-  + new lemmas `fmap_at_left0P`, and `fmap_at_right0E`.
+  + new lemmas `cvgDl`, `cvgDr`, `cvgBl`, `cvgBr`, `cvg0D`, `cvg0DC`, 
+    `cvgD0`, `cvgCD0`, `cvg0B`, `cvg0BC`, `cvgB0`, `cvgCB0`, `cvgN0`, `fmap_at_left0P`, and `fmap_at_right0E`.
 - in file `tvs.v`,
   + new lemmas `near_shiftE`, and `nearZE`.
 
+- in `derive.v`
+  + new lemmas `derive1Dn`, `der1_scaleLR`, `deriveZLR`, `derivableZLR`, 
+    `derivable_shiftf`, `derive_shiftf`, `is_derive_shiftf`, `derive1_shiftf`, 
+    `near_eq_derive1n_near`, `near_eq_derive1_near`, `near_eq_derive1n`, and 
+    `near_eq_derive1`.
+
+- in file `exp.v`,
+  + new lemmas `cvgy_expR`, `cvgNy_expR`, `lny`, `Nlt1_powR_cvg0`, 
+    `expMexpR_cvgr0`, `powRMexpR_cvgr0`, `expMpowR_cvgr0`, and 
+    `expMexpr_cvgn0`.
+
 ### Changed
 
 - in `realsum.v`:
diff --git a/theories/exp.v b/theories/exp.v
index 9546f690e1..5ea7229cc9 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -517,6 +517,16 @@ under eq_cvg do rewrite -mulNrn -mulr_natr expRM_natr; apply: cvg_expr.
 by rewrite ger0_norm ?expR_ge0// expRN invf_lt1 ?expR_gt1// expR_gt0.
 Qed.
 
+Lemma cvgy_expR : @expR R @ +oo --> +oo.
+Proof.
+apply: ger_cvgy.
+- apply: nearW; exact: expR_ge1Dx.
+- exact: cvg_addrl.
+Qed. 
+
+Lemma cvgNy_expR : @expR R @ -oo --> 0.
+Proof. apply/cvgNy_compNP; exact: cvgr_expR. Qed.
+
 Lemma expR_inj : injective (@expR R).
 Proof.
 move=> x y exE.
@@ -819,6 +829,13 @@ apply/cvgrNyPle => y; near=> x; rewrite -ler_expR lnK; first by rewrite posrE.
 by near: x; apply: nbhs_right_le; exact: expR_gt0.
 Unshelve. end_near. Qed.
 
+Lemma lny : ln @ +oo --> +oo.
+Proof.
+apply/cvgryPgey.
+near=> A; near=> x.
+by rewrite -[leLHS]expRK ler_ln ?posrE// expR_gt0.
+Unshelve. all: by end_near. Qed.
+
 End Ln.
 
 Section PowR.
@@ -1089,6 +1106,19 @@ apply: (@cvg_comp _ _ _ _ _ _ (@ninfty_nbhs R)).
 exact/cvgNy_compNP/cvgr_expR.
 Unshelve. end_near. Qed.
 
+Lemma Nlt1_powR_cvg0 (z : R) : 
+  0 <= z -> z < 1 -> z `^ x @[x --> +oo] --> 0.
+Proof.
+rewrite le_eqVlt => /predU1P[<- _|z_gt0 z_lt1].
+  apply: cvg_near_cst.
+  near do by rewrite powR0// gt_eqF.
+rewrite /powR gt_eqF//.
+apply: cvg_comp (@cvgNy_expR R).
+apply: lt0_cvgMlNy.
+apply: ln_lt0.
+by apply/andP.
+Unshelve. all: by end_near. Qed.
+
 Lemma derivable_powR v x : {in `]0, +oo[, forall a, derivable (powR ^~ x) a v}.
 Proof.
 have [-> y _|] := eqVneq v 0; first exact/derivable0.
@@ -1126,6 +1156,14 @@ move=> x_gt0; split.
 by rewrite -derive1E powR_derive1// in_itv andbT.
 Qed.
 
+Global Instance is_derive1_powRl (a x : R) : 0 < a -> 
+  is_derive x 1 (powR a) (ln a * a `^ x).
+Proof.
+move=> a_gt0; rewrite /powR gt_eqF//.
+apply: is_derive_eq.
+by rewrite scaler0 add0r scaler1 mulrC.
+Qed.
+
 Lemma lt0_powR1 x p : x < 0 -> x `^ p = 1.
 Proof.
 by move=> x0; rewrite /powR lt_eqF// (ln0 (ltW x0)) mulr0 expR0.
@@ -1476,3 +1514,94 @@ by move/contra_not; apply; exact: dvg_harmonic.
 Qed.
 
 End riemannR_series.
+
+Section exponential_domination.
+Context (R : realType).
+
+Lemma expMexpR_cvgr0 (n : nat) (b : R) : 
+  b < 0 -> x ^+ n * expR (b * x) @[x --> +oo] --> 0.
+Proof.
+move=> b_lt0.
+apply: cvg_trans.
+  apply: (near_eq_cvg (f := fun x => x ^+ n / expR (- (b * x)))).
+  near=> x.
+  by rewrite expRN invrK.
+elim: n => [|n IHn].
+  under eq_cvg do rewrite expr0 div1r expRN invrK.
+  apply: cvg_comp (@cvgNy_expR _).
+  by apply: lt0_cvgMrNy.
+apply: lhopital_pinfty_at_pinfty.
+- near do exact: is_derive_exp.
+- near do exact: is_derive1_comp.
+- apply: cvg_comp (@cvgy_expR _).
+  apply/cvgNry.
+  by apply: lt0_cvgMrNy.
+- near=> x.
+  apply: mulf_neq0.
+  + by rewrite expR_eq0.
+  + by rewrite scaler1 gt_eqF// oppr_gt0.
+- apply: cvg_trans.
+    apply: near_eq_cvg.
+    near=> x.
+    by rewrite !scaler1/= (mulrC _ (- _)) -mulf_div.
+  by apply: cvgCM0.
+Unshelve. all: by end_near. Qed.
+
+Lemma powRMexpR_cvgr0 (a b : R) : b < 0 -> 
+  x `^ a * expR (b * x) @[x --> +oo] --> 0.
+Proof.
+move=> bt_gt0.
+case: (ler0P a) => [a_le0|a_gt0].
+  apply: (squeeze_cvgr (f := fun=> 0) (h := fun x => expR (b * x))).
+  - near=> x.
+    apply/andP; split.
+    + by apply: mulr_ge0 => //; exact: powR_ge0.
+    + apply: ler_piMl => //.
+      rewrite -(powRr0 x).
+      by apply: ler_powR.
+  - exact: cvg_cst.
+  - apply: cvg_comp (@cvgNy_expR _).
+    by apply: lt0_cvgMrNy.
+near \oo => n.
+apply: (squeeze_cvgr (f := fun=>0) (h := fun x => x ^+ n * expR (b * x))).
+- near=> x.
+  apply/andP; split.
+  + by apply: mulr_ge0 => //; exact: powR_ge0.
+  + rewrite -powR_mulrn// ler_pM2r ?expR_gt0//.
+    apply: ler_powR => //.
+    by near: n; exact: nbhs_infty_ger.
+- exact: cvg_cst.
+- by apply: expMexpR_cvgr0.
+Unshelve. all: by end_near. Qed.
+
+Lemma expMpowR_cvgr0 (n : nat) (z : R) : 
+  0 <= z -> z < 1 -> x ^+ n * z `^ x @[x --> +oo] --> 0.
+Proof.
+rewrite le_eqVlt => /predU1P[<- _|z_gt0 z_lt1].
+  apply: cvg_near_cst.
+  near=> x.
+  by rewrite powR0 ?mulr0// gt_eqF.
+apply: cvg_trans (expMexpR_cvgr0 n (b := ln z) _).
+- apply: near_eq_cvg.
+  near=> x.
+  congr (_ * _).
+    by rewrite /powR ifN ?(mulrC x)// gt_eqF.
+- by rewrite ln_lt0// z_gt0 z_lt1.
+Unshelve. all: by end_near. Qed.
+
+Lemma expMexpr_cvgn0 (n : nat) (z : R) : 
+  `|z| < 1 -> k%:R ^+ n * z ^+ k @[k --> \oo] --> 0.
+Proof.
+move=> Nz_lt1.
+apply: norm_cvg0.
+apply: cvg_trans.
+  apply: near_eq_cvg.
+  near=> k.
+  rewrite normrM !normrX ger0_norm => [//|].
+  by rewrite -[X in _ * X]powR_mulrn.
+apply: (cvg_comp _ (fun x => x ^+ n * `|z| `^ x)).
+  exact: cvgr_idn.
+by apply: expMpowR_cvgr0.
+Unshelve. all: by end_near. Qed.
+
+End exponential_domination.