From c9d765028eef006cbefc6dc9df6ee1d6b41b57ae Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 14 Feb 2025 11:28:14 +0900 Subject: [PATCH] Boost near_derive Simpler proof of a stronger version of near_derive --- theories/derive.v | 59 ++++++++++++++++++------------------------- theories/normedtype.v | 5 ++++ 2 files changed, 29 insertions(+), 35 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index c7a7517e4..b4885b486 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1861,52 +1861,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. diff --git a/theories/normedtype.v b/theories/normedtype.v index 171b7196d..bd0ddac6c 100644 --- a/theories/normedtype.v +++ b/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}