Boost near_derive

Simpler proof of a stronger version of near_derive

Author: CohenCyril

theories/derive.v

@@ -1863,42 +1863,30 @@ Qed.
 
 Lemma near_derive (R : numFieldType) (V W : normedModType R)
     (f g : V -> W) (a v : V) : v != 0 -> {near a, f =1 g} ->
-  {near 0^', (fun h => h^-1 *: (f (h *: v + a) - f a)) =1
-             (fun h => h^-1 *: (g (h *: v + a) - g a))}.
-Proof.
-move=> v0 nfg; near=> t; congr (_ *: _).
-near: t.
-move: nfg; 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.
+   \forall h \near 0,
+     h^-1 *: (f (h *: v + a) - f a) = h^-1 *: (g (h *: v + a) - g a).
+Proof.
+move=> v0 fg; near do rewrite (nbhs_singleton fg) (near fg)// addrC.
+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)
     (f g : V -> W) (a v : V) : v != 0 ->
   {near a, f =1 g} -> derivable f a v -> derivable g a v.
 Proof.
 move=> vn0 nfg /cvg_ex[/= l fl]; apply/cvg_ex; exists l => /=.
-by apply: cvg_trans fl; apply: near_eq_cvg; exact: near_derive.
+by apply: cvg_trans fl; apply: near_eq_cvg; apply/cvg_within/near_derive.
 Qed.
 
 Lemma near_eq_derive (R : numFieldType) (V W : normedModType R)
   (f g : V -> W) (a v : V) :
   v != 0 -> (\near a, f a = g a) -> 'D_v f a = 'D_v g a.
 Proof.
 move=> v0 fg; rewrite /derive; congr (lim _).
-have {}fg := near_derive v0 fg.
-rewrite eqEsubset; split; apply: near_eq_cvg=> //.
-by move/filterS : fg; apply => ? /esym.
-Qed.
+rewrite eqEsubset; split; apply/near_eq_cvg; apply/cvg_within/near_derive => //.
+by near do apply/esym.
+Unshelve. all: by end_near. Qed.
 
 Lemma near_eq_is_derive (R : numFieldType) (V W : normedModType R)
     (f g : V -> W) (a v : V) (df : W) : v != 0 ->

theories/normedtype.v

@@ -5406,6 +5406,11 @@ rewrite propeqE; split=> /= /nbhs_normP [_/posnumP[e] ye];
 apply/nbhs_normP; exists e%:num => //= t et.
   by apply: ye; rewrite /= distrC addrCA [x + _]addrC addrK distrC.
 by have /= := ye (t - (x - y)); rewrite opprB addrCA subrKA addrNK; exact.
+
+Lemma near0Z {R : numFieldType} {V : tvsType R} (y : V) (P : set V) :
+  (\forall x \near 0, P x) -> (\forall k \near 0, P (k *: y)).
+Proof.
+by have /= := @scalel_continuous R V y 0 _; rewrite scale0r; apply.
 Qed.
 
 Lemma cvg_comp_shift {T : Type} {K : numDomainType} {R : normedModType K}