From c6e349f8973a3fdf819152b3c4de5f8eaeeb01ce Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 12:59:46 +0200 Subject: [PATCH 1/3] Move `is_deriveV` and `is_derive1_comp` to `derive.v` --- theories/derive.v | 18 ++++++++++++++++++ theories/realfun.v | 19 ------------------- 2 files changed, 18 insertions(+), 19 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index 07a7aa7cab..83fd93f025 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1398,6 +1398,15 @@ move=> df dg; apply/cvg_ex; exists (- (f x) ^- 2 *: 'D_v f x). exact: der_inv. Qed. +Lemma is_deriveV f (x v : V) (df : R) : + f x != 0 -> is_derive x v f df -> + is_derive x v (fun y => (f y)^-1) (- (f x) ^- 2 *: df). +Proof. +move=> fxNZ Df. +constructor; first by apply: derivableV => //; case: Df. +by rewrite deriveV //; case: Df => _ ->. +Qed. + End Derive_lemmasVR. Lemma derive_shift {R : numFieldType} (v k : R) : @@ -2068,6 +2077,15 @@ rewrite diff_comp // !derive1E' //= -[X in 'd _ _ X = _]mulr1. by rewrite [LHS]linearZ mulrC. Qed. +Global Instance is_derive1_comp (R : realFieldType) (f g : R -> R) (x a b : R) : + is_derive (g x) 1 f a -> is_derive x 1 g b -> is_derive x 1 (f \o g) (a * b). +Proof. +move=> [fgxv <-{a}] [gv <-{b}]; apply: (@DeriveDef _ _ _ _ _ (f \o g)). + apply/derivable1_diffP/differentiable_comp; first exact/derivable1_diffP. + by move/derivable1_diffP in fgxv. +by rewrite -derive1E (derive1_comp gv fgxv) 2!derive1E. +Qed. + Lemma near_eq_growth_rate (R : numFieldType) (V W : normedModType R) (f g : V -> W) (a v : V) : {near a, f =1 g} -> \forall h \near 0, diff --git a/theories/realfun.v b/theories/realfun.v index dd0e368af8..d2a1326c3d 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1872,25 +1872,6 @@ apply/continuous_subspaceT=> r. exact/differentiable_continuous/derivable1_diffP. Qed. -Global Instance is_derive1_comp (f g : R -> R) (x a b : R) : - is_derive (g x) 1 f a -> is_derive x 1 g b -> - is_derive x 1 (f \o g) (a * b). -Proof. -move=> [fgxv <-{a}] [gv <-{b}]; apply: (@DeriveDef _ _ _ _ _ (f \o g)). - apply/derivable1_diffP/differentiable_comp; first exact/derivable1_diffP. - by move/derivable1_diffP in fgxv. -by rewrite -derive1E (derive1_comp gv fgxv) 2!derive1E. -Qed. - -Lemma is_deriveV (f : R -> R) (x t v : R) : - f x != 0 -> is_derive x v f t -> - is_derive x v (fun y => (f y)^-1) (- (f x) ^- 2 *: t). -Proof. -move=> fxNZ Df. -constructor; first by apply: derivableV => //; case: Df. -by rewrite deriveV //; case: Df => _ ->. -Qed. - Lemma is_derive_inverse (f g : R -> R) l x : {near x, cancel f g} -> {near x, continuous f} -> From f285a9728179fda6f02eacbaf5cb7dbc7a3e401c Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 13:03:07 +0200 Subject: [PATCH 2/3] Update changelog --- CHANGELOG_UNRELEASED.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2d85fdc0a5..bcaa2e9242 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -354,6 +354,9 @@ - in `classical_sets.v` + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) +- moved from `realfun.v` to `derive.v`: + + lemmas `is_deriveV`, `is_derive1_comp`. + ### Renamed - in `tvs.v`: From 8a1248c3d3b141ae426492b70c3d759677b52104 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 19 Jul 2026 21:30:17 +0900 Subject: [PATCH 3/3] nitpicks --- CHANGELOG_UNRELEASED.md | 4 ++-- theories/derive.v | 12 +++++++----- theories/realfun.v | 3 --- 3 files changed, 9 insertions(+), 10 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index bcaa2e9242..23a78527d4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -354,8 +354,8 @@ - in `classical_sets.v` + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) -- moved from `realfun.v` to `derive.v`: - + lemmas `is_deriveV`, `is_derive1_comp`. +- moved from `realfun.v` to `derive.v` and generalized: + + lemmas `is_deriveV`, `is_derive1_comp` ### Renamed diff --git a/theories/derive.v b/theories/derive.v index 83fd93f025..aadc6c86c9 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1287,7 +1287,7 @@ by apply/funext => x; rewrite derive1E deriveB// derive_id derive_cst sub0r. Qed. Section Derive_lemmasVR. -Variables (R : numFieldType) (V : normedModType R). +Context {R : numFieldType} {V : normedModType R}. Implicit Types (f g : V -> R) (x v : V). Fact der_mult f g x v : @@ -1398,17 +1398,19 @@ move=> df dg; apply/cvg_ex; exists (- (f x) ^- 2 *: 'D_v f x). exact: der_inv. Qed. -Lemma is_deriveV f (x v : V) (df : R) : +Lemma is_deriveV f x v (df : R) : f x != 0 -> is_derive x v f df -> is_derive x v (fun y => (f y)^-1) (- (f x) ^- 2 *: df). Proof. -move=> fxNZ Df. -constructor; first by apply: derivableV => //; case: Df. -by rewrite deriveV //; case: Df => _ ->. +move=> fxNZ Df; apply: DeriveDef; first exact: derivableV. +by rewrite deriveV//; case: Df => _ ->. Qed. End Derive_lemmasVR. +#[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) => + (apply: is_deriveV; first by []) : typeclass_instances. + Lemma derive_shift {R : numFieldType} (v k : R) : 'D_v (shift k : R -> R) = cst v. Proof. diff --git a/theories/realfun.v b/theories/realfun.v index d2a1326c3d..6c0bad1d2c 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1931,9 +1931,6 @@ Lemma derive_sqrt {K : realType} (r : K) : 0 < r -> 'D_1 Num.sqrt r = (2 * Num.sqrt r)^-1. Proof. by move=> r0; exact/derive_val/is_derive1_sqrt. Qed. -#[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) => - (eapply is_deriveV; first by []) : typeclass_instances. - Section total_variation_realFieldType. Context {R : realFieldType}. Implicit Types (a b : R) (f : R -> R).