From 4c34222c2525429b2ab690d9a6d5d5017534385d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 14 Feb 2025 11:28:14 +0900 Subject: [PATCH 1/2] near lemmas about derivation Co-authored-by: Takafumi Saikawa --- CHANGELOG_UNRELEASED.md | 3 +++ theories/derive.v | 47 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 50 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f15c915450..8a408d5557 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -119,6 +119,9 @@ - new file `measurable_realfun.v` + with as contents the first half of the file `lebesgue_measure.v` +- in `derive.v`: + + lemmas `near_derive`, `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 index 9bbfe99c26..c494153df0 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1861,6 +1861,53 @@ rewrite diff_comp // !derive1E' //= -[X in 'd _ _ X = _]mulr1. by rewrite [LHS]linearZ mulrC. 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. +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. +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. + +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=> v0 fg [fav <-]; rewrite (near_eq_derive v0 fg). +by apply: DeriveDef => //; exact: near_eq_derivable fav. +Qed. + (* 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. From 1d420200b6987392f8389c7e787366b21c71029e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 19 Feb 2025 16:06:37 +0900 Subject: [PATCH 2/2] addressing comments --- CHANGELOG_UNRELEASED.md | 2 +- theories/derive.v | 35 +++++++++---------- theories/topology_theory/topology_structure.v | 2 +- 3 files changed, 19 insertions(+), 20 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8a408d5557..eb08591b9f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -120,7 +120,7 @@ + with as contents the first half of the file `lebesgue_measure.v` - in `derive.v`: - + lemmas `near_derive`, `near_eq_derivable`, `near_eq_derive`, `near_eq_is_derive` + + lemmas `near_eq_derivable`, `near_eq_derive`, `near_eq_is_derive` ### Changed diff --git a/theories/derive.v b/theories/derive.v index c494153df0..c106e58cc5 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1861,14 +1861,17 @@ rewrite diff_comp // !derive1E' //= -[X in 'd _ _ X = _]mulr1. by rewrite [LHS]linearZ mulrC. Qed. -Lemma near_derive (R : numFieldType) (V W : normedModType R) - (f g : V -> W) (a v : V) : v != 0 -> {near a, f =1 g} -> +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. -move=> v0 nfg; near=> t; congr (_ *: _). -near: t. -move: nfg; rewrite {1}/prop_near1/= nbhsE/= => -[B [oB Ba] /[dup] Bfg Bfg']. +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. @@ -1882,32 +1885,28 @@ apply: Bfg; apply: (eB (`|x| * `|2 *: v|)). by rewrite normrZ ltr_pMl ?normr_gt0// gtr0_norm ?ltr1n. 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. +Lemma near_eq_derivable : derivable f a v -> derivable g a v. Proof. -move=> vn0 nfg /cvg_ex[/= l fl]; apply/cvg_ex; exists l => /=. +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 (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. +Lemma near_eq_derive : 'D_v f a = 'D_v g a. Proof. -move=> v0 fg; rewrite /derive; congr (lim _). -have {}fg := near_derive v0 fg. +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 (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. +Lemma near_eq_is_derive (df : W) : is_derive a v f df -> is_derive a v g df. Proof. -move=> v0 fg [fav <-]; rewrite (near_eq_derive v0 fg). +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 index 1b6b57aae1..3b2d09806c 100644 --- 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.