Boost near_derive

CHANGELOG_UNRELEASED.md

@@ -96,6 +96,12 @@
   + `lebesgue_integral_differentiation.v`
   + `lebesgue_integral.v`
 
+- in `normedtype.v`:
+  + lemma `near0Z`
+
+- in `derive.v`:
+  + lemma `near_derive`
+
 ### Changed
 
 - file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package

theories/derive.v

@@ -1871,52 +1871,41 @@ 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.
+Lemma near_derive (R : numFieldType) (V W : normedModType R)
+    (f g : V -> W) (a v : V) : v != 0 -> {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).
+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 : derivable f a v -> derivable g a v.
+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=> /cvg_ex[/= l fl]; apply/cvg_ex; exists l => /=.
-by apply: cvg_trans fl; apply: near_eq_cvg; exact: near_derive.
+move=> vn0 nfg /cvg_ex[/= l fl]; apply/cvg_ex; exists l => /=.
+by apply: cvg_trans fl; apply: near_eq_cvg; apply/cvg_within/near_derive.
 Qed.
 
-Lemma near_eq_derive : 'D_v f a = 'D_v g a.
+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.
-rewrite /derive; congr (lim _).
-have {}fg := near_derive.
-rewrite eqEsubset; split; apply: near_eq_cvg=> //.
-by move/filterS : fg; apply => ? /esym.
-Qed.
+move=> v0 fg; rewrite /derive; congr (lim _).
+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 (df : W) : is_derive a v f df -> is_derive a v g df.
+Lemma near_eq_is_derive (R : numFieldType) (V W : normedModType R)
+    (f g : V -> W) (a v : V) (df : W) : v != 0 ->
+  (\near a, f a = g a) -> is_derive a v f df -> is_derive a v g df.
 Proof.
-move=> [fav <-]; rewrite near_eq_derive.
+move=> v0 fg [fav <-]; rewrite (near_eq_derive v0 fg).
 by apply: DeriveDef => //; exact: near_eq_derivable fav.
 Qed.
 
-End near_derive.
-
 Lemma derive1N {R : realFieldType} (f : R -> R) (x : R) :
   derivable f x 1 -> (- f)^`() x = (- f^`()%classic x).
 Proof. by move=> fx; rewrite !derive1E deriveN. Qed.

theories/normedtype.v

@@ -5395,6 +5395,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}