From 1eace3e518b5139aaf59cb6fdc2e358af5a599d6 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 1/9] 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 922611f3a6..b2aa465a0b 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -470,6 +470,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.
@@ -1317,6 +1320,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.
 
@@ -1484,6 +1539,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.
@@ -1514,6 +1601,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.
@@ -2185,6 +2276,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.
@@ -2609,4 +2724,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 901e7afde4ef9b083a7d74f017a01be012682301 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 2/9] Update changelog

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

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 729be117dd..01b5f1751c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -43,6 +43,11 @@
 
 - in `topology_structure.v`:
   + lemma `id_continuous`
+- 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
 
@@ -58,6 +63,9 @@
 - moved from `trigo.v` to `trigonometry_functions.v`:
   + all contents except lemmas `integral0_oneDsqr`, `integral0y_oneDsqr`
 
+- moved from `realfun.v` to `derive.v`: 
+  + lemmas `is_deriveV`, `is_derive1_comp`.
+
 ### Renamed
 
 - in `esum.v`:

From 9dee877a0a81d8904de3677905a9ac2bfbce4885 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 3/9] Add dependency on #2029 for CI

---
 CHANGELOG_UNRELEASED.md                       |  7 +++++++
 theories/derive.v                             | 19 ++++++++-----------
 .../probability_theory/beta_distribution.v    |  1 -
 3 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 01b5f1751c..cb12059759 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -43,6 +43,13 @@
 
 - in `topology_structure.v`:
   + lemma `id_continuous`
+- 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/derive.v b/theories/derive.v
index b2aa465a0b..4e9a67555a 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -1336,8 +1336,8 @@ apply: cvg_trans.
 apply: cvgD.
 - apply: cvgZ; first exact: der_k.
   apply: (cvg_comp _ _ (G := nbhs x)).
-  + apply: cvg0DC.
-    apply: cvg0MC.
+  + apply: cvg0D => //.
+    apply: (@cvg0M _ _ _ _ _ _ 1) => //.
     by apply: cvg_within_filter.
   + change (continuous_at x f).
     by apply/differentiable_continuous/derivable1_diffP.
@@ -1346,15 +1346,12 @@ apply: cvgD.
 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).
+  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.
+move=> [der_k <-] [der_f <-]/=; apply: DeriveDef.
+- exact: cvgP (der1_scaleLR _ _).
+- by apply: norm_cvg_lim; exact: cvg_trans (der1_scaleLR _ _).
 Qed.
 
 Lemma deriveZLR (k : R -> R) (f : R -> V) (x : R) : 
@@ -2724,4 +2721,4 @@ move=> dfx dgx; apply: DiffDef; first exact: differentiable_row_mx.
 by rewrite diff_row_mx// !diff_val.
 Qed.
 
-End is_diff_row_mx.
\ No newline at end of file
+End is_diff_row_mx.
diff --git a/theories/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v
index f5dbeb5643..7e7fc15dbb 100644
--- a/theories/probability_theory/beta_distribution.v
+++ b/theories/probability_theory/beta_distribution.v
@@ -78,7 +78,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 b98e893211293f3101cf75bca092346cebd09607 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 4/9] Add dependency on #2027 for CI

---
 CHANGELOG_UNRELEASED.md                 | 10 ++++++++++
 theories/topology_theory/nat_topology.v | 12 ++++++++++++
 2 files changed, 22 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index cb12059759..d457adf240 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -43,6 +43,14 @@
 
 - in `topology_structure.v`:
   + lemma `id_continuous`
+- 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`.
@@ -72,6 +80,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/nat_topology.v b/theories/topology_theory/nat_topology.v
index 9f2a95bf90..54816e6a06 100644
--- a/theories/topology_theory/nat_topology.v
+++ b/theories/topology_theory/nat_topology.v
@@ -102,6 +102,18 @@ split => [[N _ /= NP]|].
 by apply: filterS => N; exact.
 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.
 

From 2640da392e3869f593b168635dc338ed548c3a0a 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 5/9] Correct dependency to #2024

---
 CHANGELOG_UNRELEASED.md                     | 122 +++++++++++++++++++-
 classical/filter.v                          |   3 +-
 theories/topology_theory/metric_structure.v |  27 +++++
 theories/topology_theory/nat_topology.v     |  12 --
 4 files changed, 148 insertions(+), 16 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index d457adf240..abdd468db0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -11,6 +11,126 @@
   + lemmas `cvg1M`, `cvgM1`, `cvg0M`, `cvgM0`
   + lemmas `cvg1Z`, `cvg0Z`, `cvgZ0`
 
+- in `normed_module.v`:
+  + structure `NormedVector`
+  + notation `normedVectType`
+  + definition `max_space`
+  + lemmas `sup_closed_ball_compact`, `equivalence_norms`,
+    `linear_findim_continuous`
+
+- in `tvs.v`:
+  + lemmas `cvg_sum`, `sum_continuous`
+
+- in `classical_sets.v`:
+  + lemmas `setI_closed_setT`, `setI_closed_set0`
+
+- in `measurable_function.v`:
+  + lemma `g_sigma_algebra_preimage_comp`
+
+- in `measure_function.v`:
+  + lemma `g_sigma_algebra_finite_measure_unique`
+
+- new file `independence.v`:
+  + definition `independent_events`
+  + definition `mutual_independence`
+  + lemma `eq_mutual_independence`
+  + definition `independence2`, `independence2P`
+  + lemma `mutual_independence_fset`
+  + lemma `mutual_independence_finiteS`
+  + theorem `mutual_independence_finite_g_sigma`
+  + lemma `mutual_dependence_bigcup`
+  + definition `independent_RVs`
+  + lemma `independent_RVsD1`
+  + theorem `independent_generators`
+  + definition `independent_RVs2`
+  + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`,
+    `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`,
+    `independent_RVs2_funrpospos`
+  + definition `pairRV`, lemma `measurable_pairRV`
+  + lemmas `independent_RVs2_product_measure1`
+  + lemmas `independent_RVs2_setI_preimage`,
+    `independent_Lfun1_expectation_product_measure_lty`
+  + lemma `ge0_independent_expectationM`
+  + lemmas `independent_Lfun1_expectationM_lty`, `independent_Lfun1M`,
+    `independent_expectationM`
+
+- in `ereal.v`:
+  + lemma `ge0_addBefctE`
+
+- in `measure_extension.v`:
+  + definition `caratheodory_measure`
+- in `measurable_structure.v`:
+  + structure `PMeasurable`, notation `pmeasurableType`
+
+- in `subspace_topology.v`:
+  + lemma `withinU_continuous_patch`
+- in `matrix_normedtype.v`:
+  + lemma `continuous_mx`
+
+- in `derive.v`:
+  + instance `is_derive_mx`
+  + fact `dmx`
+  + lemma `diffmx`
+  + lemma `is_diff_mx`
+  + instance `is_diff_mx`
+- in `realsum.v`:
+  + lemma `esum_psum`
+  + lemma `esum_sum`
+
+- in `constructive_ereal.v`:
+  + definition `esg`
+  + lemmas `numEesg`, `gte0_esg`, `lte0_esg`, `esg0`
+
+- in `esum.v`:
+  + lemmas `esum_eq0P`, `esumZ`, `exchange_esum`
+  + lemmas `le_esum`, `esumN`
+  + lemmas `summable_le_esum`, `summable_esum_funepos`, `summable_esumN`,
+    `summableZ`, `summable_esumZ`
+  + lemmas `esum_if_eq_op`
+  + lemmas `exchange_esum_ereal_sup`
+
+- in `ereal.v`:
+  + lemmas `exchange_ereal_sup`, `ge0_ereal_supZl`, `ge0_ereal_supZl_range`
+
+- in `sequences.v`:
+  + lemmas `ereal_supD`, `ereal_sup_sum`
+
+- in `reals.v`:
+  + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn`
+- in `mathcomp_extra.v`:
+  + lemmas `divDl_ge0`, `divDl_le1`
+
+- in `unstable.v`:
+  + lemmas `divD_onem`
+
+- 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`
+
+- in `tvs.v`:
+  + structure `SubConvexTvs`, notation `subConvexTvsType`
+
+- in `normed_module.v`:
+  + structure `SubNormedModule`, notation `subNormedModType`
+  + instance `ent_xsection_filter`
+  + light-weigth factory `subLmodule_isSubNormedmodule`
+
+- new file `hahn_banach_theorem.v`:
+  + module `LinearGraph`
+    * definitions `graph`, `linear_graph`
+    * lemmas `lingraph_00`, `lingraphZ`, `lingraphD`
+  + module `HahnBanachZorn`
+    * definitions `extend_graph`, `le_graph`, `functional_graph`, `le_extend_graph`
+    * record `zorn_type`
+    * definition `zphi`
+    * lemma `zorn_type_eq`
+    * definition `zornS`
+    * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness`
+  + theorems `hahn_banach_extension`, `hahn_banach_extension_normed`
 - in `normal_distribution.v`:
   + definition `post_stddev`
   + lemmas `post_stddev_gt0`, `post_stddevE`
@@ -80,8 +200,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 d679d446e8..9617295dcc 100644
--- a/classical/filter.v
+++ b/classical/filter.v
@@ -1280,8 +1280,7 @@ Qed.
 
 (* For using near on sets in a filter *)
 Section NearSet.
-Context {Y : Type}.
-Context (F : set_system Y) (PF : ProperFilter F).
+Context {Y : Type} (F : set_system Y) (PF : ProperFilter F).
 
 Definition powerset_filter_from : set_system (set Y) := filter_from
   [set M | [/\ M `<=` F,
diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v
index 38e3025416..a64e3e9eb3 100644
--- a/theories/topology_theory/metric_structure.v
+++ b/theories/topology_theory/metric_structure.v
@@ -314,6 +314,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 54816e6a06..9f2a95bf90 100644
--- a/theories/topology_theory/nat_topology.v
+++ b/theories/topology_theory/nat_topology.v
@@ -102,18 +102,6 @@ split => [[N _ /= NP]|].
 by apply: filterS => N; exact.
 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.
 

From ff5d949c045d60335c8558c81c2e2d9e79869e8f Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 16 Aug 2026 17:22:01 +0900
Subject: [PATCH 6/9] fix after rebase, linting, minor gen

---
 CHANGELOG_UNRELEASED.md                     | 132 ++--------------
 theories/derive.v                           | 162 +++++++++-----------
 theories/topology_theory/metric_structure.v |  27 ----
 3 files changed, 81 insertions(+), 240 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index abdd468db0..7b87631c18 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -11,126 +11,6 @@
   + lemmas `cvg1M`, `cvgM1`, `cvg0M`, `cvgM0`
   + lemmas `cvg1Z`, `cvg0Z`, `cvgZ0`
 
-- in `normed_module.v`:
-  + structure `NormedVector`
-  + notation `normedVectType`
-  + definition `max_space`
-  + lemmas `sup_closed_ball_compact`, `equivalence_norms`,
-    `linear_findim_continuous`
-
-- in `tvs.v`:
-  + lemmas `cvg_sum`, `sum_continuous`
-
-- in `classical_sets.v`:
-  + lemmas `setI_closed_setT`, `setI_closed_set0`
-
-- in `measurable_function.v`:
-  + lemma `g_sigma_algebra_preimage_comp`
-
-- in `measure_function.v`:
-  + lemma `g_sigma_algebra_finite_measure_unique`
-
-- new file `independence.v`:
-  + definition `independent_events`
-  + definition `mutual_independence`
-  + lemma `eq_mutual_independence`
-  + definition `independence2`, `independence2P`
-  + lemma `mutual_independence_fset`
-  + lemma `mutual_independence_finiteS`
-  + theorem `mutual_independence_finite_g_sigma`
-  + lemma `mutual_dependence_bigcup`
-  + definition `independent_RVs`
-  + lemma `independent_RVsD1`
-  + theorem `independent_generators`
-  + definition `independent_RVs2`
-  + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`,
-    `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`,
-    `independent_RVs2_funrpospos`
-  + definition `pairRV`, lemma `measurable_pairRV`
-  + lemmas `independent_RVs2_product_measure1`
-  + lemmas `independent_RVs2_setI_preimage`,
-    `independent_Lfun1_expectation_product_measure_lty`
-  + lemma `ge0_independent_expectationM`
-  + lemmas `independent_Lfun1_expectationM_lty`, `independent_Lfun1M`,
-    `independent_expectationM`
-
-- in `ereal.v`:
-  + lemma `ge0_addBefctE`
-
-- in `measure_extension.v`:
-  + definition `caratheodory_measure`
-- in `measurable_structure.v`:
-  + structure `PMeasurable`, notation `pmeasurableType`
-
-- in `subspace_topology.v`:
-  + lemma `withinU_continuous_patch`
-- in `matrix_normedtype.v`:
-  + lemma `continuous_mx`
-
-- in `derive.v`:
-  + instance `is_derive_mx`
-  + fact `dmx`
-  + lemma `diffmx`
-  + lemma `is_diff_mx`
-  + instance `is_diff_mx`
-- in `realsum.v`:
-  + lemma `esum_psum`
-  + lemma `esum_sum`
-
-- in `constructive_ereal.v`:
-  + definition `esg`
-  + lemmas `numEesg`, `gte0_esg`, `lte0_esg`, `esg0`
-
-- in `esum.v`:
-  + lemmas `esum_eq0P`, `esumZ`, `exchange_esum`
-  + lemmas `le_esum`, `esumN`
-  + lemmas `summable_le_esum`, `summable_esum_funepos`, `summable_esumN`,
-    `summableZ`, `summable_esumZ`
-  + lemmas `esum_if_eq_op`
-  + lemmas `exchange_esum_ereal_sup`
-
-- in `ereal.v`:
-  + lemmas `exchange_ereal_sup`, `ge0_ereal_supZl`, `ge0_ereal_supZl_range`
-
-- in `sequences.v`:
-  + lemmas `ereal_supD`, `ereal_sup_sum`
-
-- in `reals.v`:
-  + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn`
-- in `mathcomp_extra.v`:
-  + lemmas `divDl_ge0`, `divDl_le1`
-
-- in `unstable.v`:
-  + lemmas `divD_onem`
-
-- 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`
-
-- in `tvs.v`:
-  + structure `SubConvexTvs`, notation `subConvexTvsType`
-
-- in `normed_module.v`:
-  + structure `SubNormedModule`, notation `subNormedModType`
-  + instance `ent_xsection_filter`
-  + light-weigth factory `subLmodule_isSubNormedmodule`
-
-- new file `hahn_banach_theorem.v`:
-  + module `LinearGraph`
-    * definitions `graph`, `linear_graph`
-    * lemmas `lingraph_00`, `lingraphZ`, `lingraphD`
-  + module `HahnBanachZorn`
-    * definitions `extend_graph`, `le_graph`, `functional_graph`, `le_extend_graph`
-    * record `zorn_type`
-    * definition `zphi`
-    * lemma `zorn_type_eq`
-    * definition `zornS`
-    * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness`
-  + theorems `hahn_banach_extension`, `hahn_banach_extension_normed`
 - in `normal_distribution.v`:
   + definition `post_stddev`
   + lemmas `post_stddev_gt0`, `post_stddevE`
@@ -180,9 +60,12 @@
 
 - in `derive.v`
   + new lemmas `derive1Dn`, `der1_scaleLR`, `deriveZLR`, `derivableZLR`, 
+- in `derive.v`:
+  + 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`.
+    `near_eq_derive1n_near`, `near_eq_derive1_near`, `near_eq_derive1n`,
+    `near_eq_derive1`
+  + global instance `is_derive_exp`
 
 ### Changed
 
@@ -199,7 +82,7 @@
   + all contents except lemmas `integral0_oneDsqr`, `integral0y_oneDsqr`
 
 - moved from `realfun.v` to `derive.v`: 
-  + lemmas `is_deriveV`, `is_derive1_comp`.
+  + lemmas `is_deriveV`, `is_derive1_comp`
 
 ### Renamed
 
@@ -232,6 +115,9 @@
 
 - from `pseudometric_normed_Zmodule.v` to `topology_structure.v`:
   + lemma `continuous_comp_cvg`
+- in `derive.v`:
+  + lemmas `derive1_comp`, `is_derive1_comp` (`realFieldType` -> `numFieldType`)
+  + lemmas `derive_shift`, `is_derive_shift` (function codomain)
 
 ### Deprecated
 
diff --git a/theories/derive.v b/theories/derive.v
index 4e9a67555a..3de3a988d1 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -470,7 +470,7 @@ 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).
+Lemma derive1Dn V (f : R -> V) m n : f^`(n + m) = f^`(m)^`(n).
 Proof. by rewrite /derive1n iterD. Qed.
 
 End DifferentialR2.
@@ -480,7 +480,7 @@ Notation "f ^` ( n )" := (derive1n n f) : classical_set_scope.
 Notation derivemxE := deriveEjacobian (only parsing).
 
 Section DifferentialR3.
-Variable R : numFieldType.
+Context {R : numFieldType}.
 
 Fact dcst (V W : normedModType R) (a : W) (x : V) : continuous (0 : V -> W) /\
   cst a \o shift x = cst (cst a x) + \0 +o_ 0 id.
@@ -1320,32 +1320,35 @@ 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) 
+Lemma derive_cst (k : W) (x v : V) : 'D_v (cst k) x = 0.
+Proof. by rewrite derive_val. Qed.
+
+End Derive_lemmasVW.
+
+Section Derive_LR.
+Context {R : numFieldType} {V : normedModType R}.
+Implicit Types (k : R -> R) (f : R -> V) (x : R).
+
+Lemma der1_scaleLR k f x : derivable k x 1 -> derivable f x 1 ->
+  h^-1 *: (((fun x0 => 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.
+move=> der_k der_f/=; rewrite (@near_eq_cvg_eq _ _ _ _ _
+    (fun h => (h^-1 * (k (h%:A + x) - k x)) *: f (h%:A + x) +
+              k x *: (h^-1 *: (f (h%:A + x) - f x)))).
   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.
+  rewrite scalerA (mulrC (k x)) -(scalerA h^-1 (k x)) -scalerA -scalerDr.
+  by congr (_ *: _); rewrite scalerBl scalerBr addrA subrK.
 apply: cvgD.
-- apply: cvgZ; first exact: der_k.
-  apply: (cvg_comp _ _ (G := nbhs x)).
-  + apply: cvg0D => //.
-    apply: (@cvg0M _ _ _ _ _ _ 1) => //.
-    by apply: cvg_within_filter.
-  + change (continuous_at x f).
-    by apply/differentiable_continuous/derivable1_diffP.
-- apply: cvgZl_tmp.
-    exact: der_f.
+- apply/(cvgZ der_k)/(@cvg_comp _ _ _ _ _ _ (nbhs x)).
+  + apply: cvg0D => //;  apply: (@cvg0M _ _ _ _ _ _ 1) => //.
+    exact: cvg_within_filter.
+  + rewrite -/(continuous_at x f).
+    exact/differentiable_continuous/derivable1_diffP.
+- exact: cvgZl_tmp der_f.
 Unshelve. all: by end_near. Qed.
 
-Global Instance is_derive1ZLR (k : R -> R) (f : R -> V) (x dk : R) (df : V) :
+Global Instance is_derive1ZLR k f 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.
@@ -1354,25 +1357,15 @@ move=> [der_k <-] [der_f <-]/=; apply: DeriveDef.
 - by apply: norm_cvg_lim; exact: cvg_trans (der1_scaleLR _ _).
 Qed.
 
-Lemma deriveZLR (k : R -> R) (f : R -> V) (x : R) : 
-  derivable k x 1 -> derivable f x 1 ->
+Lemma deriveZLR k f x : 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.
+Proof. by move=> dk df; exact/derive_val/is_derive1ZLR. Qed.
 
-Lemma derive_cst (k : W) (x v : V) : 'D_v (cst k) x = 0.
-Proof. by rewrite derive_val. Qed.
+Lemma derivableZLR k f x : derivable k x 1 -> derivable f x 1 ->
+  derivable (fun x => k x *: f x) x 1.
+Proof. by move=> dk df; exact/ex_derive/is_derive1ZLR; apply: derivableP. Qed.
 
-End Derive_lemmasVW.
+End Derive_LR.
 
 Section derive_id.
 Variables (R : numFieldType) (V : normedModType R).
@@ -1526,46 +1519,36 @@ End Derive_lemmasVR.
 #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
   (apply: is_deriveV; first by []) : typeclass_instances.
 
-Lemma derive_shift {R : numFieldType} (v k : R) :
-  'D_v (shift k : R -> R) = cst v.
+Lemma derive_shift {R : numFieldType} {V : normedModType R} (v k : V) :
+  'D_v (shift k : V -> V) = cst v.
 Proof.
 by apply/funext => x/=; rewrite deriveD// derive_id derive_cst addr0.
 Qed.
 
-Lemma is_derive_shift {R : numFieldType} x v (k : R) :
+Lemma is_derive_shift {R : numFieldType} {V : normedModType R} x (v k : V) :
   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).
+Context {R : numFieldType} {V : normedModType R} (f : R -> V).
+Implicit Types x a v : R.
 
-Lemma derivable_shiftf x a v : 
+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.
+Proof. by rewrite {1}/derivable/=; 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 derive_shiftf x a v : 'D_v (f \o shift a) x = 'D_v f (x + a).
+Proof. by rewrite /derive/=; under [in RHS]eq_fun do rewrite addrA. Qed.
+
+Lemma derive1_shiftf x a : (f \o shift a)^`() x = f^`() (x + a).
+Proof. by rewrite 2!derive1E derive_shiftf. Qed.
 
-Lemma is_derive_shiftf x a (df : V) : 
+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.
+by move=> [/derivable_shiftf derf] <-; split => //; rewrite derive_shiftf.
 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 :
@@ -1600,7 +1583,7 @@ 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.
+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.
@@ -1810,8 +1793,7 @@ by exists c => //; rewrite in_itv /= ltW (itvP cab).
 Qed.
 
 Section ger0_derive1_le.
-Context {R : realType}.
-Variables (f : R -> R) (a b : R).
+Context {R : realType} (f : R -> R) (a b : R).
 Hypothesis df : forall x, x \in `]a, b[%R -> derivable f x 1.
 Hypothesis dfge0 : forall x, x \in `]a, b[%R -> 0 <= f^`() x.
 
@@ -1853,8 +1835,7 @@ Proof. by rewrite -continuous_open_subspace//; exact: ger0_derive1_le. Qed.
 End ger0_derive1_le.
 
 Section ler0_derive1_le.
-Context {R : realType}.
-Variables (f : R -> R) (a b : R).
+Context {R : realType} (f : R -> R) (a b : R).
 Hypothesis df : forall x, x \in `]a, b[%R -> derivable f x 1.
 Hypothesis dfle0 : forall x, x \in `]a, b[%R -> f^`() x <= 0.
 
@@ -1904,8 +1885,7 @@ by apply: ler0_derive1_le_cc; [ exact: df | exact: dfle0 | by [] | | | by [] ];
 Qed.
 
 Section gtr0_derive1_lt.
-Context {R : realType}.
-Variables (f : R -> R) (a b : R).
+Context {R : realType} (f : R -> R) (a b : R).
 Hypothesis df : forall x, x \in `]a, b[%R -> derivable f x 1.
 Hypothesis dfgt0 : forall x, x \in `]a, b[%R -> 0 < f^`() x.
 
@@ -2217,7 +2197,7 @@ apply: (@decr_derive1_le0_itvNy _ _ b1 _ _ _ _ zNyb).
 - by move=> x y Dx Dy yx; rewrite ltrN2; apply: incrf.
 Qed.
 
-Lemma derive1_comp (R : realFieldType) (f g : R -> R) x :
+Lemma derive1_comp {R : numFieldType} (f g : R -> R) x :
   derivable f x 1 -> derivable g (f x) 1 ->
   (g \o f)^`() x = g^`()%classic (f x) * f^`()%classic x.
 Proof.
@@ -2227,7 +2207,7 @@ 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) :
+Global Instance is_derive1_comp {R : numFieldType} (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)).
@@ -2236,7 +2216,7 @@ move=> [fgxv <-{a}] [gv <-{b}]; apply: (@DeriveDef _ _ _ _ _ (f \o g)).
 by rewrite -derive1E (derive1_comp gv fgxv) 2!derive1E.
 Qed.
 
-Lemma near_eq_growth_rate (R : numFieldType) (V W : normedModType R)
+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,
      h^-1 *: (f (h *: v + a) - f a) = h^-1 *: (g (h *: v + a) - g a).
@@ -2246,7 +2226,7 @@ apply/(@near0Z _ _ _ [set v | (a + v) \is_near (nbhs a)])=> /=.
 by rewrite (near_shift a)/=; near do rewrite /= sub0r addrC addrNK//.
 Unshelve. all: by end_near. Qed.
 
-Lemma near_eq_derivable (R : numFieldType) (V W : normedModType R)
+Lemma near_eq_derivable {R : numFieldType} {V W : normedModType R}
     (f g : V -> W) (a v : V) :
   {near a, f =1 g} -> derivable f a v -> derivable g a v.
 Proof.
@@ -2255,7 +2235,7 @@ move=> vn0 nfg /cvg_ex[/= l fl]; apply/cvg_ex; exists l => /=.
 exact/(cvg_trans _ fl)/near_eq_cvg/cvg_within/near_eq_growth_rate.
 Qed.
 
-Lemma near_eq_derive (R : numFieldType) (V W : normedModType R)
+Lemma near_eq_derive {R : numFieldType} {V W : normedModType R}
   (f g : V -> W) (a v : V) :
   (\near a, f a = g a) -> 'D_v f a = 'D_v g a.
 Proof.
@@ -2265,7 +2245,7 @@ rewrite eqEsubset; split; apply/near_eq_cvg/cvg_within/near_eq_growth_rate =>//.
 by near do apply/esym.
 Unshelve. all: by end_near. Qed.
 
-Lemma near_eq_is_derive (R : numFieldType) (V W : normedModType R)
+Lemma near_eq_is_derive {R : numFieldType} {V W : normedModType R}
     (f g : V -> W) (a v : V) (df : W) :
   (\near a, f a = g a) -> is_derive a v f df -> is_derive a v g df.
 Proof.
@@ -2273,30 +2253,32 @@ 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)}.
+Section near_eq_derive1.
+Context {R : numFieldType} {V : normedModType R}.
+Implicit Types (f g : R -> V) (x : R).
+
+Lemma near_eq_derive1n_near n f g x:
+  {near x, f =1 g} -> {near x, f^`(n) =1 g^`(n)}.
 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.
+move=> fg; elim: n => [//|n IH].
+near do (rewrite 2!derive1nS !derive1E; apply: near_eq_derive).
+by rewrite near_nbhs; exact: near_join.
 Unshelve. all: by end_near. Qed.
 
-Lemma near_eq_derive1_near (R : numFieldType) (V : normedModType R) (f g : R -> V) (x : R) :
+Lemma near_eq_derive1_near f g x :
   {near x, f =1 g} -> {near x, f^`() =1 g^`()}.
-Proof. rewrite -!derive1n1; exact: near_eq_derive1n_near. Qed.
+Proof. by 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_derive1n n f g x :
+  {near x, f =1 g} -> f^`(n) x = g^`(n) x.
+Proof. by move=> /near_eq_derive1n_near => /(_ n)/nbhs_singleton. Qed.
 
-Lemma near_eq_derive1 (R : numFieldType) (V : normedModType R) (f g : R -> V) (x : R) : 
+Lemma near_eq_derive1 f g x :
   {near x, f =1 g} -> f^`() x = g^`() x.
 Proof. by rewrite -!derive1n1; exact: near_eq_derive1n. Qed.
 
+End near_eq_derive1.
+
 Section Derive_max.
 Context {K : realType} {V W : normedModType K}.
 Implicit Types f g : V -> K^o.
diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v
index a64e3e9eb3..38e3025416 100644
--- a/theories/topology_theory/metric_structure.v
+++ b/theories/topology_theory/metric_structure.v
@@ -314,33 +314,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).
 

From a8123f963886eaa0c3b289085a8b498b96f3f339 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 16 Aug 2026 17:24:09 +0900
Subject: [PATCH 7/9] nitpick

---
 theories/derive.v | 24 ++++++++++--------------
 1 file changed, 10 insertions(+), 14 deletions(-)

diff --git a/theories/derive.v b/theories/derive.v
index 3de3a988d1..0506f7b5d0 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -265,7 +265,7 @@ by apply/eqolim0P; apply: (cvg_trans (dfc 0)); rewrite linear0.
 Unshelve. all: by end_near. Qed.
 
 Section littleo_lemmas.
-Variables (X Y Z : normedModType R).
+Context {X Y Z : normedModType R}.
 
 Lemma normm_littleo x (f : X -> Y) : `| [o_(x \near x) (1 : R) of f x]| = 0.
 Proof.
@@ -581,7 +581,7 @@ Unshelve. all: by end_near. Qed.
 End DifferentialR3.
 
 Section DifferentialR3_numFieldType.
-Variable R : numFieldType.
+Context {R : numFieldType}.
 
 Lemma littleo_linear0 (V W : normedModType R) (f : {linear V -> W}) :
   (f : V -> W) =o_ 0 id -> f = cst 0 :> (V -> W).
@@ -1107,7 +1107,7 @@ Proof. by move=> /differentiableP df; rewrite diff_val. Qed.
 End DifferentialR3_numFieldType.
 
 Section DeriveRU.
-Variables (R : numFieldType) (U : normedModType R).
+Context {R : numFieldType} {U : normedModType R}.
 Implicit Types f : R -> U.
 
 Let der1 f x : derivable f x 1 ->
@@ -1164,7 +1164,7 @@ Qed.
 End DeriveRU.
 
 Section DeriveVW.
-Variables (R : numFieldType) (V W : normedModType R).
+Context {R : numFieldType} {V W : normedModType R}.
 Implicit Types f : V -> W.
 
 Lemma derivable1P f x v :
@@ -1368,7 +1368,7 @@ Proof. by move=> dk df; exact/ex_derive/is_derive1ZLR; apply: derivableP. Qed.
 End Derive_LR.
 
 Section derive_id.
-Variables (R : numFieldType) (V : normedModType R).
+Context {R : numFieldType} {V : normedModType R}.
 
 Lemma derivable_id (x v : V) : derivable id x v.
 Proof. exact/diff_derivable. Qed.
@@ -1940,8 +1940,7 @@ move=> abf abf' cf x y ax xy yb; apply: (@gtr0_derive1_lt_cc _ _ a b) => //;
 Qed.
 
 Section ltr0_derive1_lt.
-Context {R : realType}.
-Variables (f : R -> R) (a b : R).
+Context {R : realType} (f : R -> R) (a b : R).
 Hypothesis df : forall x, x \in `]a, b[%R -> derivable f x 1.
 Hypothesis dflt0 : forall x, x \in `]a, b[%R -> f^`() x < 0.
 
@@ -2265,16 +2264,13 @@ near do (rewrite 2!derive1nS !derive1E; apply: near_eq_derive).
 by rewrite near_nbhs; exact: near_join.
 Unshelve. all: by end_near. Qed.
 
-Lemma near_eq_derive1_near f g x :
-  {near x, f =1 g} -> {near x, f^`() =1 g^`()}.
+Lemma near_eq_derive1_near f g x : {near x, f =1 g} -> {near x, f^`() =1 g^`()}.
 Proof. by rewrite -!derive1n1; exact: near_eq_derive1n_near. Qed.
 
-Lemma near_eq_derive1n n f g x :
-  {near x, f =1 g} -> f^`(n) x = g^`(n) x.
+Lemma near_eq_derive1n n f g x : {near x, f =1 g} -> f^`(n) x = g^`(n) x.
 Proof. by move=> /near_eq_derive1n_near => /(_ n)/nbhs_singleton. Qed.
 
-Lemma near_eq_derive1 f g x :
-  {near x, f =1 g} -> f^`() x = g^`() x.
+Lemma near_eq_derive1 f g x : {near x, f =1 g} -> f^`() x = g^`() x.
 Proof. by rewrite -!derive1n1; exact: near_eq_derive1n. Qed.
 
 End near_eq_derive1.
@@ -2380,7 +2376,7 @@ Lemma trigger_derive (R : realType) (f : R -> R) x x1 y1 :
 Proof. by move=> Hi <-. Qed.
 
 Section derive_horner.
-Variable (R : realFieldType).
+Context {R : realFieldType}.
 Local Open Scope ring_scope.
 
 Lemma horner0_ext : horner (0 : {poly R}) = 0.

From bfb4e9712f4ae40c689450732952500817de3f83 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 16 Aug 2026 17:44:33 +0900
Subject: [PATCH 8/9] renaming

---
 CHANGELOG_UNRELEASED.md |  3 ++-
 theories/derive.v       | 25 ++++++++++++++-----------
 theories/ftc.v          | 20 ++++++++------------
 3 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 7b87631c18..408aeb7da9 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -62,10 +62,11 @@
   + new lemmas `derive1Dn`, `der1_scaleLR`, `deriveZLR`, `derivableZLR`, 
 - in `derive.v`:
   + lemmas `derive1Dn`, `der1_scaleLR`, `deriveZLR`, `derivableZLR`, 
-    `derivable_shiftf`, `derive_shiftf`, `is_derive_shiftf`, `derive1_shiftf`, 
+    `derivable_comp_shift`, `derive_comp_shift`, `is_derive_comp_shift`, `derive1_comp_shift`, 
     `near_eq_derive1n_near`, `near_eq_derive1_near`, `near_eq_derive1n`,
     `near_eq_derive1`
   + global instance `is_derive_exp`
+  + lemma `derive1_shift`
 
 ### Changed
 
diff --git a/theories/derive.v b/theories/derive.v
index 0506f7b5d0..bf30479a4c 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -1525,31 +1525,34 @@ Proof.
 by apply/funext => x/=; rewrite deriveD// derive_id derive_cst addr0.
 Qed.
 
+Lemma derive1_shift {R : numFieldType} (k : R) : (shift k)^`() = cst 1.
+Proof. by rewrite -(derive_shift _ k); apply/funext => x; rewrite derive1E. Qed.
+
 Lemma is_derive_shift {R : numFieldType} {V : normedModType R} x (v k : V) :
   is_derive x v (shift k) v.
 Proof. by apply: DeriveDef => //; rewrite derive_val addr0. Qed.
 
-Section derive_shiftf.
+Section derive_comp_shift.
 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. by rewrite {1}/derivable/=; 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).
+Lemma derive_comp_shift x a v : 'D_v (f \o shift a) x = 'D_v f (x + a).
 Proof. by rewrite /derive/=; under [in RHS]eq_fun do rewrite addrA. Qed.
 
-Lemma derive1_shiftf x a : (f \o shift a)^`() x = f^`() (x + a).
-Proof. by rewrite 2!derive1E derive_shiftf. Qed.
+Lemma derive1_comp_shift x a : (f \o shift a)^`() x = f^`() (x + a).
+Proof. by rewrite 2!derive1E derive_comp_shift. Qed.
+
+Lemma derivable_comp_shift x a v :
+  derivable f (x + a) v -> derivable (f \o shift a) x v.
+Proof. by rewrite {1}/derivable/=; under eq_is_cvg do rewrite addrA. Qed.
 
-Lemma is_derive_shiftf x a (df : V) :
+Lemma is_derive_comp_shift x a (df : V) :
   is_derive (x + a) 1 f df -> is_derive x 1 (f \o shift a) df.
 Proof.
-by move=> [/derivable_shiftf derf] <-; split => //; rewrite derive_shiftf.
+by move=> [/derivable_comp_shift derf] <-; split => //; rewrite derive_comp_shift.
 Qed.
 
-End derive_shiftf.
+End derive_comp_shift.
 
 Lemma derive1_cst {R : numFieldType} (V : normedModType R) (k : V) t :
   (cst k)^`() t = 0.
diff --git a/theories/ftc.v b/theories/ftc.v
index 7145c6ed5a..c5655ddf23 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -1796,17 +1796,15 @@ Lemma ge0_integration_by_substitution_shift_itvy (f : R -> R) (r e : R) :
   \int[mu]_(x in `[r, +oo[) ((f \o shift e) x)%:E)%E.
 Proof.
 move=> cf f0.
-have dshiftE : (shift e)^`() = cst 1.
-  by apply/funext => x; rewrite derive1E -(derive_shift 1 e).
 rewrite (@increasing_ge0_integration_by_substitutiony _ (shift e))//=.
 - by move=> x y _ _ xy; rewrite ltr_leD.
-- by rewrite dshiftE; apply: in1W; exact: cst_continuous.
-- by rewrite dshiftE.
-- by rewrite dshiftE.
+- by rewrite derive1_shift; apply: in1W; exact: cst_continuous.
+- by rewrite derive1_shift.
+- by rewrite derive1_shift.
 - split; first by move=> x _; exact: ex_derive.
   by apply/cvg_at_right_filter; exact: cvgD.
 - exact: cvg_addrr.
-by rewrite dshiftE mulr1.
+by rewrite derive1_shift mulr1.
 Qed.
 
 Lemma ge0_integration_by_substitution_shift_itvNy (f : R -> R) (r e : R) :
@@ -1816,17 +1814,15 @@ Lemma ge0_integration_by_substitution_shift_itvNy (f : R -> R) (r e : R) :
    \int[mu]_(x in `]-oo, r]) ((f \o shift e) x)%:E)%E.
 Proof.
 move=> cf f0.
-have dshiftE : (shift e)^`() = cst 1.
-  by apply/funext => x; rewrite derive1E -(derive_shift 1 e).
 rewrite (@increasing_ge0_integration_by_substitutionNy _ (shift e))//.
 - by move=> x y _ _ xy; rewrite ltr_leD.
-- by rewrite dshiftE; apply: in1W; exact: cst_continuous.
-- by rewrite dshiftE.
-- by rewrite dshiftE.
+- by rewrite derive1_shift; apply: in1W; exact: cst_continuous.
+- by rewrite derive1_shift.
+- by rewrite derive1_shift.
 - split; first by move=> x _; exact: ex_derive.
   by apply/cvg_at_left_filter; exact: cvgD.
 - exact: cvg_addrr_Ny.
-by rewrite dshiftE mulr1.
+by rewrite derive1_shift mulr1.
 Qed.
 
 End ge0_integration_by_substitution_shift.

From 2d3225173625e892b23a5f2e014a50a36efbc351 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 16 Aug 2026 18:06:51 +0900
Subject: [PATCH 9/9] fix changelog

---
 CHANGELOG_UNRELEASED.md | 14 --------------
 1 file changed, 14 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 408aeb7da9..bdba2409cd 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -43,20 +43,6 @@
 
 - in `topology_structure.v`:
   + lemma `id_continuous`
-- 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`.
-- 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`,