From b9976523367206d33ccc5c64ca6bdda122549bcf Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 14 Feb 2025 11:28:14 +0900 Subject: [PATCH 1/7] 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 2a9f2df94d..d22ca34160 100644 --- a/theories/derive.v +++ b/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. diff --git a/theories/normedtype.v b/theories/normedtype.v index f5a6be0a66..ca67c83a36 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5396,6 +5396,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} From 53071c1eab39a7afedb822caeb32efdfc8653ad1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 10 Apr 2025 22:57:02 +0900 Subject: [PATCH 2/7] changelog --- CHANGELOG_UNRELEASED.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b42fe43edd..fbf0b77398 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -111,6 +111,11 @@ - in `real_interval.v`: + lemma `itvNycEbigcap` +- in `normedtype.v`: + + lemma `near0Z` + +- in `derive.v`: + + lemma `near_derive` ### Changed From b9de1a109185f698f8b45a414061c9cd249f2937 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 11 Apr 2025 09:41:54 +0200 Subject: [PATCH 3/7] Update theories/normedtype.v --- theories/normedtype.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/normedtype.v b/theories/normedtype.v index ca67c83a36..983f3aff68 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5396,6 +5396,7 @@ 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. +Qed. 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)). From 63618e006c91f3e07506d33febf559f597eef67c Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 11 Apr 2025 13:50:16 +0200 Subject: [PATCH 4/7] renamings --- theories/derive.v | 2 +- theories/normedtype.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index d22ca34160..9f94f34bfe 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1871,7 +1871,7 @@ rewrite diff_comp // !derive1E' //= -[X in 'd _ _ X = _]mulr1. by rewrite [LHS]linearZ mulrC. Qed. -Lemma near_derive (R : numFieldType) (V W : normedModType R) +Lemma near_eq_growth_rate (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). diff --git a/theories/normedtype.v b/theories/normedtype.v index 983f3aff68..babdbde12f 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5398,7 +5398,7 @@ apply/nbhs_normP; exists e%:num => //= t et. by have /= := ye (t - (x - y)); rewrite opprB addrCA subrKA addrNK; exact. Qed. -Lemma near0Z {R : numFieldType} {V : tvsType R} (y : V) (P : set V) : +Lemma near0Z {R : numFieldType} {V : normedModType 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. From 47f57f3d41eacd1aad47b59404d19b2a470f4e4a Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 11 Apr 2025 14:24:01 +0200 Subject: [PATCH 5/7] fix --- theories/derive.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index 9f94f34bfe..6ef8677b95 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1886,7 +1886,7 @@ Lemma near_eq_derivable (R : numFieldType) (V W : normedModType R) {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; apply/cvg_within/near_derive. +exact/(cvg_trans _ fl)/near_eq_cvg/cvg_within/near_eq_growth_rate. Qed. Lemma near_eq_derive (R : numFieldType) (V W : normedModType R) @@ -1894,7 +1894,7 @@ Lemma near_eq_derive (R : numFieldType) (V W : normedModType R) v != 0 -> (\near a, f a = g a) -> 'D_v f a = 'D_v g a. Proof. move=> v0 fg; rewrite /derive; congr (lim _). -rewrite eqEsubset; split; apply/near_eq_cvg; apply/cvg_within/near_derive => //. +rewrite eqEsubset; split; apply/near_eq_cvg/cvg_within/near_eq_growth_rate => //. by near do apply/esym. Unshelve. all: by end_near. Qed. From c8a3d10bd62fb884ebe5d4a42293c2e51f354c05 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 11 Apr 2025 14:53:56 +0200 Subject: [PATCH 6/7] update toolbox --- .nix/coq-nix-toolbox.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 47eb2317dd..8cfef937ab 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"60657f676e682de3e6a2f5d553aa737bf6801efd" +"36b6af97e5de62782c4cc0dfdda3a40e64d668ad" From bf7e63540cfcee782aafa7d533c3e740dcf0563b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 15 Apr 2025 15:55:30 +0900 Subject: [PATCH 7/7] upd changelog --- CHANGELOG_UNRELEASED.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fbf0b77398..cac0e65551 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -115,7 +115,7 @@ + lemma `near0Z` - in `derive.v`: - + lemma `near_derive` + + lemma `near_eq_growth_rate` ### Changed