near lemmas about derivation (#1477)

* near lemmas about derivation --------- Co-authored-by: Takafumi Saikawa <[email protected]>
math-comp · Feb 19, 2025 · 762e08b · 762e08b
1 parent 9863f51
commit 762e08b
Show file tree

Hide file tree

Showing 3 changed files with 50 additions and 1 deletion.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -211,6 +211,9 @@
   + definitions `PosNum`, `NngNum`, `posnum_spec` and `nonneg_spec`
   + lemmas `posnumP` and `nonnegP`
 
+- in `derive.v`:
+  + lemmas `near_eq_derivable`, `near_eq_derive`, `near_eq_is_derive`
+
 ### Changed
 
 - in `lebesgue_integral.v`

diff --git a/theories/derive.v b/theories/derive.v
@@ -1861,6 +1861,52 @@ rewrite diff_comp // !derive1E' //= -[X in 'd  _ _ X = _]mulr1.
 by rewrite [LHS]linearZ mulrC.
 Qed.
 
+Section near_derive.
+Context (R : numFieldType) (V W : normedModType R).
+Variables (f g : V -> W) (a v : V).
+Hypotheses (v0 : v != 0) (afg : {near a, f =1 g}).
+
+Let near_derive :
+  {near 0^', (fun h => h^-1 *: (f (h *: v + a) - f a)) =1
+             (fun h => h^-1 *: (g (h *: v + a) - g a))}.
+Proof.
+near do congr (_ *: _).
+move: afg; rewrite {1}/prop_near1/= nbhsE/= => -[B [oB Ba] /[dup] Bfg Bfg'].
+have [e /= e0 eB] := open_subball oB Ba.
+have vv0 : 0 < `|2 *: v| by rewrite normrZ mulr_gt0 ?normr_gt0.
+near=> x.
+have x0 : 0 < `|x| by rewrite normr_gt0//; near: x; exact: nbhs_dnbhs_neq.
+congr (_ - _); last exact: Bfg'.
+apply: Bfg; apply: (eB (`|x| * `|2 *: v|)).
+- rewrite /ball_/= sub0r normrN normrM !normr_id -ltr_pdivlMr//.
+  by near: x; apply: dnbhs0_lt; rewrite divr_gt0.
+- by rewrite mulr_gt0.
+- rewrite -ball_normE/= opprD addrCA subrr addr0 normrN normrZ ltr_pM2l//.
+  by rewrite normrZ ltr_pMl ?normr_gt0// gtr0_norm ?ltr1n.
+Unshelve. all: by end_near. Qed.
+
+Lemma near_eq_derivable : derivable f a v -> derivable g a v.
+Proof.
+move=> /cvg_ex[/= l fl]; apply/cvg_ex; exists l => /=.
+by apply: cvg_trans fl; apply: near_eq_cvg; exact: near_derive.
+Qed.
+
+Lemma near_eq_derive : 'D_v f a = 'D_v g a.
+Proof.
+rewrite /derive; congr (lim _).
+have {}fg := near_derive.
+rewrite eqEsubset; split; apply: near_eq_cvg=> //.
+by move/filterS : fg; apply => ? /esym.
+Qed.
+
+Lemma near_eq_is_derive (df : W) : is_derive a v f df -> is_derive a v g df.
+Proof.
+move=> [fav <-]; rewrite near_eq_derive.
+by apply: DeriveDef => //; exact: near_eq_derivable fav.
+Qed.
+
+End near_derive.
+
 (* Trick to trigger type class resolution *)
 Lemma trigger_derive (R : realType) (f : R -> R) x x1 y1 :
   is_derive x (1 : R) f x1 -> x1 = y1 -> is_derive x 1 f y1.

diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
@@ -104,7 +104,7 @@ HB.structure Definition PointedTopological :=
   {T of PointedNbhs T & Nbhs_isTopological T}.
 
 #[short(type="bpTopologicalType")]
-HB.structure Definition BiPointedTopological := 
+HB.structure Definition BiPointedTopological :=
   { X of BiPointed X & Topological X }.
 
 Section Topological1.