From 64f2ba076dcf400a55340706ad0a46d0c9b4da6b Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 22 Jan 2026 18:34:21 +0100 Subject: [PATCH 1/4] chore: a few more lemmas --- Mathlib/Analysis/Calculus/Deriv/Pow.lean | 28 ++---- Mathlib/Analysis/Calculus/FDeriv/Pow.lean | 87 ++++++------------- .../Calculus/IteratedDeriv/Lemmas.lean | 40 ++------- 3 files changed, 42 insertions(+), 113 deletions(-) diff --git a/Mathlib/Analysis/Calculus/Deriv/Pow.lean b/Mathlib/Analysis/Calculus/Deriv/Pow.lean index baaaa3d6c3c8ca..45ceb9dbdd634e 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Pow.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Pow.lean @@ -105,33 +105,21 @@ theorem HasDerivWithinAt.fun_pow (h : HasDerivWithinAt f f' s x) (n : ℕ) : theorem HasDerivWithinAt.pow (h : HasDerivWithinAt f f' s x) (n : ℕ) : HasDerivWithinAt (f ^ n) (n * f x ^ (n - 1) * f') s x := h.fun_pow n -theorem HasDerivAt.fun_pow (h : HasDerivAt f f' x) (n : ℕ) : - HasDerivAt (fun x ↦ f x ^ n) (n * f x ^ (n - 1) * f') x := by - simpa using h.hasFDerivAt.pow n |>.hasDerivAt - +@[to_fun HasDerivAt.fun_pow] theorem HasDerivAt.pow (h : HasDerivAt f f' x) (n : ℕ) : - HasDerivAt (f ^ n) (n * f x ^ (n - 1) * f') x := h.fun_pow n + HasDerivAt (f ^ n) (n * f x ^ (n - 1) * f') x := by + simpa using h.hasFDerivAt.pow n |>.hasDerivAt -@[simp] -theorem derivWithin_fun_pow (h : DifferentiableWithinAt 𝕜 f s x) (n : ℕ) : - derivWithin (fun x => f x ^ n) s x = n * f x ^ (n - 1) * derivWithin f s x := by +@[to_fun (attr := simp) derivWithin_fun_pow] +theorem derivWithin_pow (h : DifferentiableWithinAt 𝕜 f s x) (n : ℕ) : + derivWithin (f ^ n) s x = n * f x ^ (n - 1) * derivWithin f s x := by by_cases hsx : UniqueDiffWithinAt 𝕜 s x · exact (h.hasDerivWithinAt.pow n).derivWithin hsx · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx] -@[simp] -theorem derivWithin_pow (h : DifferentiableWithinAt 𝕜 f s x) (n : ℕ) : - derivWithin (f ^ n) s x = n * f x ^ (n - 1) * derivWithin f s x := - derivWithin_fun_pow h n - -@[simp] -theorem deriv_fun_pow (h : DifferentiableAt 𝕜 f x) (n : ℕ) : - deriv (fun x => f x ^ n) x = n * f x ^ (n - 1) * deriv f x := - (h.hasDerivAt.pow n).deriv - -@[simp] +@[to_fun (attr := simp) deriv_fun_pow] theorem deriv_pow (h : DifferentiableAt 𝕜 f x) (n : ℕ) : - deriv (f ^ n) x = n * f x ^ (n - 1) * deriv f x := deriv_fun_pow h n + deriv (f ^ n) x = n * f x ^ (n - 1) * deriv f x := (h.hasDerivAt.pow n).deriv end NormedCommRing diff --git a/Mathlib/Analysis/Calculus/FDeriv/Pow.lean b/Mathlib/Analysis/Calculus/FDeriv/Pow.lean index 89baf5759dbd1d..568c6cabdeeb39 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Pow.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Pow.lean @@ -45,60 +45,51 @@ private theorem aux (f : E → 𝔸) (f' : E →L[𝕜] 𝔸) (x : E) (n : ℕ) simp only [Finset.mem_range, Nat.lt_succ_iff] at hx rw [tsub_add_eq_add_tsub hx] -theorem HasStrictFDerivAt.fun_pow' (h : HasStrictFDerivAt f f' x) (n : ℕ) : - HasStrictFDerivAt (fun x ↦ f x ^ n) +@[to_fun] +theorem HasStrictFDerivAt.pow' (h : HasStrictFDerivAt f f' x) (n : ℕ) : + HasStrictFDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x := match n with | 0 => by simpa using hasStrictFDerivAt_const 1 x | 1 => by simpa using h | n + 1 + 1 => by - have := h.mul' (h.fun_pow' (n + 1)) + have := h.mul' (h.pow' (n + 1)) simp_rw [pow_succ' _ (n + 1)] refine this.congr_fderiv <| aux _ _ _ _ -theorem HasStrictFDerivAt.pow' (h : HasStrictFDerivAt f f' x) (n : ℕ) : - HasStrictFDerivAt (f ^ n) - (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x := h.fun_pow' n - theorem hasStrictFDerivAt_pow' (n : ℕ) {x : 𝔸} : HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ x ^ n) (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 _ <• x ^ i) x := hasStrictFDerivAt_id _ |>.pow' n -theorem HasFDerivWithinAt.fun_pow' (h : HasFDerivWithinAt f f' s x) (n : ℕ) : - HasFDerivWithinAt (fun x ↦ f x ^ n) +@[to_fun] +theorem HasFDerivWithinAt.pow' (h : HasFDerivWithinAt f f' s x) (n : ℕ) : + HasFDerivWithinAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) s x := match n with | 0 => by simpa using hasFDerivWithinAt_const 1 x s | 1 => by simpa using h | n + 1 + 1 => by - have := h.mul' (h.fun_pow' (n + 1)) + have := h.mul' (h.pow' (n + 1)) simp_rw [pow_succ' _ (n + 1)] exact this.congr_fderiv <| aux _ _ _ _ -theorem HasFDerivWithinAt.pow' (h : HasFDerivWithinAt f f' s x) (n : ℕ) : - HasFDerivWithinAt (f ^ n) - (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) s x := h.fun_pow' n - theorem hasFDerivWithinAt_pow' (n : ℕ) {x : 𝔸} {s : Set 𝔸} : HasFDerivWithinAt (𝕜 := 𝕜) (fun x ↦ x ^ n) (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 _ <• x ^ i) s x := hasFDerivWithinAt_id _ _ |>.pow' n -theorem HasFDerivAt.fun_pow' (h : HasFDerivAt f f' x) (n : ℕ) : - HasFDerivAt (fun x ↦ f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x := +@[to_fun] +theorem HasFDerivAt.pow' (h : HasFDerivAt f f' x) (n : ℕ) : + HasFDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x := match n with | 0 => by simpa using hasFDerivAt_const 1 x | 1 => by simpa using h | n + 1 + 1 => by - have := h.mul' (h.fun_pow' (n + 1)) + have := h.mul' (h.pow' (n + 1)) simp_rw [pow_succ' _ (n + 1)] exact this.congr_fderiv <| aux _ _ _ _ -theorem HasFDerivAt.pow' (h : HasFDerivAt f f' x) (n : ℕ) : - HasFDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x := - h.fun_pow' n - theorem hasFDerivAt_pow' (n : ℕ) {x : 𝔸} : HasFDerivAt (𝕜 := 𝕜) (fun x ↦ x ^ n) (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 _ <• x ^ i) x := @@ -118,67 +109,45 @@ theorem differentiableWithinAt_pow (n : ℕ) {x : 𝔸} {s : Set 𝔸} : DifferentiableWithinAt 𝕜 (fun x : 𝔸 => x ^ n) s x := differentiableWithinAt_id.pow _ -@[simp, fun_prop] -theorem DifferentiableAt.fun_pow (hf : DifferentiableAt 𝕜 f x) (n : ℕ) : - DifferentiableAt 𝕜 (fun x => f x ^ n) x := - differentiableWithinAt_univ.mp <| hf.differentiableWithinAt.pow n - -@[simp, fun_prop] +@[to_fun (attr := simp, fun_prop)] theorem DifferentiableAt.pow (hf : DifferentiableAt 𝕜 f x) (n : ℕ) : - DifferentiableAt 𝕜 (f ^ n) x := hf.fun_pow n + DifferentiableAt 𝕜 (f ^ n) x := + differentiableWithinAt_univ.mp <| hf.differentiableWithinAt.pow n theorem differentiableAt_pow (n : ℕ) {x : 𝔸} : DifferentiableAt 𝕜 (fun x : 𝔸 => x ^ n) x := differentiableAt_id.pow _ -@[fun_prop] -theorem DifferentiableOn.fun_pow (hf : DifferentiableOn 𝕜 f s) (n : ℕ) : - DifferentiableOn 𝕜 (fun x => f x ^ n) s := fun x h => (hf x h).pow n - -@[fun_prop] +@[to_fun (attr := fun_prop)] theorem DifferentiableOn.pow (hf : DifferentiableOn 𝕜 f s) (n : ℕ) : - DifferentiableOn 𝕜 (f ^ n) s := hf.fun_pow n + DifferentiableOn 𝕜 (f ^ n) s := fun x h => (hf x h).pow n theorem differentiableOn_pow (n : ℕ) {s : Set 𝔸} : DifferentiableOn 𝕜 (fun x : 𝔸 => x ^ n) s := differentiableOn_id.pow n -@[simp, fun_prop] -theorem Differentiable.fun_pow (hf : Differentiable 𝕜 f) (n : ℕ) : - Differentiable 𝕜 fun x => f x ^ n := - fun x => (hf x).pow n - -@[simp, fun_prop] +@[to_fun (attr := simp, fun_prop)] theorem Differentiable.pow (hf : Differentiable 𝕜 f) (n : ℕ) : Differentiable 𝕜 (f ^ n) := - hf.fun_pow n + fun x => (hf x).pow n theorem differentiable_pow (n : ℕ) : Differentiable 𝕜 fun x : 𝔸 => x ^ n := differentiable_id.pow _ -theorem fderiv_fun_pow' (n : ℕ) (hf : DifferentiableAt 𝕜 f x) : - fderiv 𝕜 (fun x ↦ f x ^ n) x - = (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderiv 𝕜 f x <• f x ^ i) := - hf.hasFDerivAt.pow' n |>.fderiv - +@[to_fun fderiv_fun_pow'] theorem fderiv_pow' (n : ℕ) (hf : DifferentiableAt 𝕜 f x) : fderiv 𝕜 (f ^ n) x = (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderiv 𝕜 f x <• f x ^ i) := - fderiv_fun_pow' n hf + hf.hasFDerivAt.pow' n |>.fderiv theorem fderiv_pow_ring' {x : 𝔸} (n : ℕ) : fderiv 𝕜 (fun x : 𝔸 ↦ x ^ n) x = (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> .id _ _ <• x ^ i) := by rw [fderiv_fun_pow' n differentiableAt_fun_id, fderiv_fun_id] -theorem fderivWithin_fun_pow' (hxs : UniqueDiffWithinAt 𝕜 s x) - (n : ℕ) (hf : DifferentiableWithinAt 𝕜 f s x) : - fderivWithin 𝕜 (fun x ↦ f x ^ n) s x - = (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderivWithin 𝕜 f s x <• f x ^ i) := - hf.hasFDerivWithinAt.pow' n |>.fderivWithin hxs - +@[to_fun fderivWithin_fun_pow'] theorem fderivWithin_pow' (hxs : UniqueDiffWithinAt 𝕜 s x) (n : ℕ) (hf : DifferentiableWithinAt 𝕜 f s x) : fderivWithin 𝕜 (f ^ n) s x = (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderivWithin 𝕜 f s x <• f x ^ i) := - fderivWithin_fun_pow' hxs n hf + hf.hasFDerivWithinAt.pow' n |>.fderivWithin hxs theorem fderivWithin_pow_ring' {s : Set 𝔸} {x : 𝔸} (n : ℕ) (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (fun x : 𝔸 ↦ x ^ n) s x @@ -234,21 +203,17 @@ theorem fderiv_fun_pow (n : ℕ) (hf : DifferentiableAt 𝕜 f x) : theorem fderiv_pow (n : ℕ) (hf : DifferentiableAt 𝕜 f x) : fderiv 𝕜 (fun x ↦ f x ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x := - fderiv_fun_pow n hf + hf.hasFDerivAt.pow n |>.fderiv theorem fderiv_pow_ring {x : 𝔸} (n : ℕ) : fderiv 𝕜 (fun x : 𝔸 ↦ x ^ n) x = (n • x ^ (n - 1)) • .id _ _ := by rw [fderiv_fun_pow n differentiableAt_fun_id, fderiv_fun_id] -theorem fderivWithin_fun_pow (hxs : UniqueDiffWithinAt 𝕜 s x) - (n : ℕ) (hf : DifferentiableWithinAt 𝕜 f s x) : - fderivWithin 𝕜 (fun x ↦ f x ^ n) s x = (n • f x ^ (n - 1)) • fderivWithin 𝕜 f s x := - hf.hasFDerivWithinAt.pow n |>.fderivWithin hxs - +@[to_fun fderivWithin_fun_pow] theorem fderivWithin_pow (hxs : UniqueDiffWithinAt 𝕜 s x) (n : ℕ) (hf : DifferentiableWithinAt 𝕜 f s x) : fderivWithin 𝕜 (f ^ n) s x = (n • f x ^ (n - 1)) • fderivWithin 𝕜 f s x := - fderivWithin_fun_pow hxs n hf + hf.hasFDerivWithinAt.pow n |>.fderivWithin hxs theorem fderivWithin_pow_ring {s : Set 𝔸} {x : 𝔸} (n : ℕ) (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (fun x : 𝔸 ↦ x ^ n) s x = (n • x ^ (n - 1)) • .id _ _ := by diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean index b6222afdfc6fd8..76933237667dd5 100644 --- a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean +++ b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean @@ -245,6 +245,7 @@ theorem iteratedDerivWithin_comp_const_sub (c : 𝕜) : ext a simp [iteratedDerivWithin, iteratedFDerivWithin_comp_const_sub] +@[to_fun iteratedDerivWithin_fun_id] lemma iteratedDerivWithin_id : iteratedDerivWithin n id s x = if n = 0 then x else if n = 1 then 1 else 0 := by obtain (_ | n) := n @@ -253,10 +254,6 @@ lemma iteratedDerivWithin_id : · simp [iteratedDerivWithin_const] · exact fun y hy ↦ derivWithin_id _ _ (h.uniqueDiffWithinAt hy) -lemma iteratedDerivWithin_fun_id : - iteratedDerivWithin n (·) s x = if n = 0 then x else if n = 1 then 1 else 0 := - iteratedDerivWithin_id hx h - lemma iteratedDerivWithin_smul {f : 𝕜 → 𝔸} {g : 𝕜 → F} (hf : ContDiffWithinAt 𝕜 (↑n) f s x) (hg : ContDiffWithinAt 𝕜 (↑n) g s x) : iteratedDerivWithin n (f • g) s x = ∑ i ∈ .range (n + 1), @@ -313,16 +310,12 @@ protected lemma Filter.EventuallyEq.iteratedDeriv iteratedDeriv n f₁ =ᶠ[𝓝 x] iteratedDeriv n f₂ := by simp_all [← nhdsWithin_univ, ← iteratedDerivWithin_univ, EventuallyEq.iteratedDerivWithin] +@[to_fun iteratedDeriv_fun_add] lemma iteratedDeriv_add (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : iteratedDeriv n (f + g) x = iteratedDeriv n f x + iteratedDeriv n g x := by simpa only [iteratedDerivWithin_univ] using iteratedDerivWithin_add (Set.mem_univ _) uniqueDiffOn_univ hf hg --- TODO: `@[to_fun]` generates the wrong name. Same for the various lemmas below. -lemma iteratedDeriv_fun_add (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : - iteratedDeriv n (fun z ↦ f z + g z) x = iteratedDeriv n f x + iteratedDeriv n g x := - iteratedDeriv_add hf hg - theorem iteratedDeriv_const_add (hn : 0 < n) (c : F) : iteratedDeriv n (fun z => c + f z) x = iteratedDeriv n f x := by simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_const_add hn c @@ -331,35 +324,25 @@ theorem iteratedDeriv_const_sub (hn : 0 < n) (c : F) : iteratedDeriv n (fun z => c - f z) x = iteratedDeriv n (-f) x := by simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_const_sub hn c -@[simp] -lemma iteratedDeriv_fun_neg (n : ℕ) (f : 𝕜 → F) (a : 𝕜) : - iteratedDeriv n (fun x ↦ -(f x)) a = -(iteratedDeriv n f a) := by - simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_neg f - -@[simp] +@[simp, to_fun iteratedDeriv_fun_neg] lemma iteratedDeriv_neg (n : ℕ) (f : 𝕜 → F) (a : 𝕜) : iteratedDeriv n (-f) a = -(iteratedDeriv n f a) := by simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_neg f +attribute [simp] iteratedDeriv_fun_neg +@[to_fun iteratedDeriv_fun_sub] lemma iteratedDeriv_sub (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : iteratedDeriv n (f - g) x = iteratedDeriv n f x - iteratedDeriv n g x := by simpa only [iteratedDerivWithin_univ] using iteratedDerivWithin_sub (Set.mem_univ _) uniqueDiffOn_univ hf hg -lemma iteratedDeriv_fun_sub (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : - iteratedDeriv n (fun z ↦ f z - g z) x = iteratedDeriv n f x - iteratedDeriv n g x := - iteratedDeriv_sub hf hg - +@[to_fun iteratedDeriv_fun_const_smul] theorem iteratedDeriv_const_smul {n : ℕ} {f : 𝕜 → F} (h : ContDiffAt 𝕜 n f x) (c : R) : iteratedDeriv n (c • f) x = c • iteratedDeriv n f x := by simpa only [iteratedDerivWithin_univ] using iteratedDerivWithin_const_smul (Set.mem_univ x) uniqueDiffOn_univ c (contDiffWithinAt_univ.mpr h) -theorem iteratedDeriv_fun_const_smul {n : ℕ} {f : 𝕜 → F} (h : ContDiffAt 𝕜 n f x) (c : R) : - iteratedDeriv n (c • f ·) x = c • iteratedDeriv n f x := - iteratedDeriv_const_smul h c - /-- A variant of `iteratedDeriv_const_smul` without differentiability assumption when the scalar multiplication is by division ring elements. -/ @[simp] @@ -421,19 +404,17 @@ lemma iteratedDeriv_comp_neg (n : ℕ) (f : 𝕜 → F) (a : 𝕜) : iteratedDeriv n (fun x ↦ f (-x)) a = (-1 : 𝕜) ^ n • iteratedDeriv n f (-a) := by simp [iteratedDeriv, ← iteratedFDerivWithin_univ, iteratedFDerivWithin_comp_neg] +@[to_fun iteratedDeriv_fun_id] lemma iteratedDeriv_id {n : ℕ} {x : 𝕜} : iteratedDeriv n id x = if n = 0 then x else if n = 1 then 1 else 0 := by obtain (_ | _ | n) := n <;> simp [iteratedDeriv_succ', iteratedDeriv_const] -lemma iteratedDeriv_fun_id {n : ℕ} {x : 𝕜} : - iteratedDeriv n (fun a ↦ a) x = if n = 0 then x else if n = 1 then 1 else 0 := - iteratedDeriv_id - lemma iteratedDeriv_fun_id_zero : iteratedDeriv n (fun a ↦ a) (0 : 𝕜) = if n = 1 then 1 else 0 := by simp +contextual [iteratedDeriv_fun_id] +@[to_fun iteratedDeriv_fun_mul] lemma iteratedDeriv_mul {f g : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : iteratedDeriv n (f * g) x = ∑ i ∈ .range (n + 1), n.choose i * iteratedDeriv i f x * iteratedDeriv (n - i) g x := by @@ -445,11 +426,6 @@ theorem iteratedDeriv_pow (m : ℕ) (k : ℕ) : iteratedDeriv k (· ^ m) x = m.descFactorial k * x ^ (m - k) := by simpa using iteratedDerivWithin_pow (Set.mem_univ x) uniqueDiffOn_univ m k -lemma iteratedDeriv_fun_mul {f g : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : - iteratedDeriv n (fun x ↦ f x * g x) x = ∑ i ∈ .range (n + 1), - n.choose i * iteratedDeriv i f x * iteratedDeriv (n - i) g x := - iteratedDeriv_mul hf hg - lemma iteratedDeriv_fun_pow_zero {n m : ℕ} : iteratedDeriv n (· ^ m) (0 : 𝕜) = if n = m then m.factorial else 0 := by obtain h | h | h := lt_trichotomy n m <;> From e1a41a6797488398a1bff4b01b6440e842bc81d5 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 22 Jan 2026 22:51:38 +0100 Subject: [PATCH 2/4] fix: statement of fderiv_pow The current version is an exact duplicate of fderiv_fun_pow, likely a copy-paste error. Fix it to match what it says. --- Mathlib/Analysis/Calculus/FDeriv/Pow.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Mathlib/Analysis/Calculus/FDeriv/Pow.lean b/Mathlib/Analysis/Calculus/FDeriv/Pow.lean index 568c6cabdeeb39..f8c00125370854 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Pow.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Pow.lean @@ -197,12 +197,9 @@ theorem hasFDerivAt_pow (n : ℕ) {x : 𝔸} : (fun x : 𝔸 ↦ x ^ n) ((n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸) x := hasFDerivAt_id _ |>.pow n -theorem fderiv_fun_pow (n : ℕ) (hf : DifferentiableAt 𝕜 f x) : - fderiv 𝕜 (fun x ↦ f x ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x := - hf.hasFDerivAt.pow n |>.fderiv - +@[to_fun fderiv_fun_pow] theorem fderiv_pow (n : ℕ) (hf : DifferentiableAt 𝕜 f x) : - fderiv 𝕜 (fun x ↦ f x ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x := + fderiv 𝕜 (f ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x := hf.hasFDerivAt.pow n |>.fderiv theorem fderiv_pow_ring {x : 𝔸} (n : ℕ) : From 66ae3c6702565e3d1ca61cce4afbeab09be11d93 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 22 Jan 2026 23:03:36 +0100 Subject: [PATCH 3/4] Five more --- Mathlib/Analysis/Analytic/Constructions.lean | 54 +++++--------------- 1 file changed, 12 insertions(+), 42 deletions(-) diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean index 8e4a7cb6769404..b0d3cf783d3c00 100644 --- a/Mathlib/Analysis/Analytic/Constructions.lean +++ b/Mathlib/Analysis/Analytic/Constructions.lean @@ -972,20 +972,14 @@ theorem analyticAt_iff_analytic_smul [Module 𝕝 F] [IsBoundedSMul 𝕝 F] [IsS analyticAt_iff_analytic_fun_smul h₁f h₂f /- A function is analytic at a point iff it is analytic after multiplication - with a non-vanishing analytic function. -/ -theorem analyticAt_iff_analytic_fun_mul {f g : E → 𝕝} {z : E} (h₁f : AnalyticAt 𝕜 f z) +with a non-vanishing analytic function. -/ +@[to_fun analyticAt_iff_analytic_fun_mul] +theorem analyticAt_iff_analytic_mul {f g : E → 𝕝} {z : E} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) : - AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (fun z ↦ f z * g z) z := by + AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f * g) z := by simp_rw [← smul_eq_mul] exact analyticAt_iff_analytic_smul h₁f h₂f -/- A function is analytic at a point iff it is analytic after multiplication - with a non-vanishing analytic function. -/ -theorem analyticAt_iff_analytic_mul {f g : E → 𝕝} {z : E} (h₁f : AnalyticAt 𝕜 f z) - (h₂f : f z ≠ 0) : - AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f * g) z := - analyticAt_iff_analytic_fun_mul h₁f h₂f - /-- `f x / g x` is analytic away from `g x = 0` -/ theorem AnalyticWithinAt.div {f g : E → 𝕝} {s : Set E} {x : E} (fa : AnalyticWithinAt 𝕜 f s x) (ga : AnalyticWithinAt 𝕜 g s x) (g0 : g x ≠ 0) : @@ -1016,9 +1010,10 @@ theorem AnalyticOnNhd.div {f g : E → 𝕝} {s : Set E} -/ /-- Finite sums of analytic functions are analytic -/ -theorem Finset.analyticWithinAt_fun_sum {f : α → E → F} {c : E} {s : Set E} +@[to_fun Finset.analyticWithinAt_fun_sum] +theorem Finset.analyticWithinAt_sum {f : α → E → F} {c : E} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) : - AnalyticWithinAt 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s c := by + AnalyticWithinAt 𝕜 (∑ n ∈ N, f n) s c := by classical induction N using Finset.induction with | empty => @@ -1030,47 +1025,22 @@ theorem Finset.analyticWithinAt_fun_sum {f : α → E → F} {c : E} {s : Set E} exact (h a (Or.inl rfl)).add (hB fun b m ↦ h b (Or.inr m)) /-- Finite sums of analytic functions are analytic -/ -theorem Finset.analyticWithinAt_sum {f : α → E → F} {c : E} {s : Set E} - (N : Finset α) (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) : - AnalyticWithinAt 𝕜 (∑ n ∈ N, f n) s c := by - convert N.analyticWithinAt_fun_sum h - simp - -/-- Finite sums of analytic functions are analytic -/ -@[fun_prop] -theorem Finset.analyticAt_fun_sum {f : α → E → F} {c : E} - (N : Finset α) (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) : - AnalyticAt 𝕜 (fun z ↦ ∑ n ∈ N, f n z) c := by - simp_rw [← analyticWithinAt_univ] at h ⊢ - exact N.analyticWithinAt_fun_sum h - -/-- Finite sums of analytic functions are analytic -/ -@[fun_prop] +@[to_fun (attr := fun_prop) Finset.analyticAt_fun_sum] theorem Finset.analyticAt_sum {f : α → E → F} {c : E} (N : Finset α) (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) : AnalyticAt 𝕜 (∑ n ∈ N, f n) c := by - convert N.analyticAt_fun_sum h - simp - -/-- Finite sums of analytic functions are analytic -/ -theorem Finset.analyticOn_fun_sum {f : α → E → F} {s : Set E} - (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) : - AnalyticOn 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s := - fun z zs ↦ N.analyticWithinAt_fun_sum (fun n m ↦ h n m z zs) + simp_rw [← analyticWithinAt_univ] at h ⊢ + exact N.analyticWithinAt_sum h /-- Finite sums of analytic functions are analytic -/ +@[to_fun Finset.analyticOn_fun_sum] theorem Finset.analyticOn_sum {f : α → E → F} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) : AnalyticOn 𝕜 (∑ n ∈ N, f n) s := fun z zs ↦ N.analyticWithinAt_sum (fun n m ↦ h n m z zs) /-- Finite sums of analytic functions are analytic -/ -theorem Finset.analyticOnNhd_fun_sum {f : α → E → F} {s : Set E} - (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) : - AnalyticOnNhd 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s := - fun z zs ↦ N.analyticAt_fun_sum (fun n m ↦ h n m z zs) - -/-- Finite sums of analytic functions are analytic -/ +@[to_fun Finset.analyticOnNhd_fun_sum] theorem Finset.analyticOnNhd_sum {f : α → E → F} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) : AnalyticOnNhd 𝕜 (∑ n ∈ N, f n) s := From ac4a84c72d1a6aa651109d9a1d29cdc262b25808 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 19 May 2026 23:20:57 +0200 Subject: [PATCH 4/4] Less verbose --- Mathlib/Analysis/Calculus/Deriv/Pow.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/Calculus/Deriv/Pow.lean b/Mathlib/Analysis/Calculus/Deriv/Pow.lean index 45ceb9dbdd634e..6978c360e8b7b4 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Pow.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Pow.lean @@ -105,7 +105,7 @@ theorem HasDerivWithinAt.fun_pow (h : HasDerivWithinAt f f' s x) (n : ℕ) : theorem HasDerivWithinAt.pow (h : HasDerivWithinAt f f' s x) (n : ℕ) : HasDerivWithinAt (f ^ n) (n * f x ^ (n - 1) * f') s x := h.fun_pow n -@[to_fun HasDerivAt.fun_pow] +@[to_fun] theorem HasDerivAt.pow (h : HasDerivAt f f' x) (n : ℕ) : HasDerivAt (f ^ n) (n * f x ^ (n - 1) * f') x := by simpa using h.hasFDerivAt.pow n |>.hasDerivAt