Skip to content

Commit 88b155d

Browse files
eric-wiesereric-wieser
committed
feat: fderiv lemmas for pow (#24351)
This generalizes the lemmas about `fderiv fun x => f x ^ n` to work over arbitrary normed modules and (noncommutative) algebras. Following the convention set by the lemmas about `fderiv` and `*`, we use `'`d names for the non-commutative variants. The naming is still a little confusing around derivatives (see [#mathlib4 > deriv neg lemmas @ πŸ’¬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/deriv.20neg.20lemmas/near/514357126)), but having these results with _some_ names is better than not having them at all. Moves: - `deriv_fun_pow''` -> `deriv_fun_pow` - `deriv_pow''` -> `deriv_pow` - `deriv_pow` -> `deriv_pow_field` - `derivWithin_pow'` -> `derivWithin_pow_field` Deletions: - `deriv_pow'`
1 parent b0c2d40 commit 88b155d

File tree

10 files changed

+396
-110
lines changed

10 files changed

+396
-110
lines changed

β€ŽMathlib.leanβ€Ž

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1434,6 +1434,7 @@ import Mathlib.Analysis.Calculus.FDeriv.Measurable
14341434
import Mathlib.Analysis.Calculus.FDeriv.Mul
14351435
import Mathlib.Analysis.Calculus.FDeriv.Norm
14361436
import Mathlib.Analysis.Calculus.FDeriv.Pi
1437+
import Mathlib.Analysis.Calculus.FDeriv.Pow
14371438
import Mathlib.Analysis.Calculus.FDeriv.Prod
14381439
import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
14391440
import Mathlib.Analysis.Calculus.FDeriv.Star

β€ŽMathlib/Analysis/Calculus/Deriv/Polynomial.leanβ€Ž

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: SΓ©bastien GouΓ«zel, Eric Wieser
55
-/
66
import Mathlib.Algebra.Polynomial.AlgebraMap
77
import Mathlib.Algebra.Polynomial.Derivative
8+
import Mathlib.Analysis.Calculus.Deriv.Mul
89
import Mathlib.Analysis.Calculus.Deriv.Pow
910
import Mathlib.Analysis.Calculus.Deriv.Add
1011

β€ŽMathlib/Analysis/Calculus/Deriv/Pow.leanβ€Ž

Lines changed: 132 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -3,103 +3,169 @@ Copyright (c) 2019 SΓ©bastien GouΓ«zel. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: SΓ©bastien GouΓ«zel
55
-/
6-
import Mathlib.Analysis.Calculus.Deriv.Mul
7-
import Mathlib.Analysis.Calculus.Deriv.Comp
6+
import Mathlib.Analysis.Calculus.FDeriv.Pow
87

98
/-!
109
# Derivative of `(f x) ^ n`, `n : β„•`
1110
12-
In this file we prove that `(x ^ n)' = n * x ^ (n - 1)`, where `n` is a natural number.
11+
In this file we prove that the FrΓ©chet derivative of `fun x => f x ^ n`,
12+
where `n` is a natural number, is `n * f x ^ (n - 1) * f'`.
13+
Additionally, we prove the case for non-commutative rings (with primed names like `deriv_pow'`),
14+
where the result is instead `βˆ‘ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i`.
1315
1416
For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of
15-
`Analysis/Calculus/Deriv/Basic`.
17+
`Mathlib/Analysis/Calculus/Deriv/Basic.lean`.
1618
1719
## Keywords
1820
1921
derivative, power
2022
-/
2123

22-
universe u
23-
24-
variable {π•œ : Type u} [NontriviallyNormedField π•œ] {x : π•œ} {s : Set π•œ}
24+
variable {π•œ 𝔸 : Type*}
25+
26+
section NormedRing
27+
variable [NontriviallyNormedField π•œ] [NormedRing 𝔸]
28+
variable [NormedAlgebra π•œ 𝔸] {f : π•œ β†’ 𝔸} {f' : 𝔸} {x : π•œ} {s : Set π•œ}
29+
30+
nonrec theorem HasStrictDerivAt.fun_pow' (h : HasStrictDerivAt f f' x) (n : β„•) :
31+
HasStrictDerivAt (fun x ↦ f x ^ n)
32+
(βˆ‘ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x := by
33+
unfold HasStrictDerivAt
34+
convert h.pow' n
35+
ext
36+
simp
37+
38+
nonrec theorem HasStrictDerivAt.pow' (h : HasStrictDerivAt f f' x) (n : β„•) :
39+
HasStrictDerivAt (f ^ n)
40+
(βˆ‘ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x := h.fun_pow' n
41+
42+
nonrec theorem HasDerivWithinAt.fun_pow' (h : HasDerivWithinAt f f' s x) (n : β„•) :
43+
HasDerivWithinAt (fun x ↦ f x ^ n)
44+
(βˆ‘ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) s x := by
45+
simpa using h.hasFDerivWithinAt.pow' n |>.hasDerivWithinAt
46+
47+
nonrec theorem HasDerivWithinAt.pow' (h : HasDerivWithinAt f f' s x) (n : β„•) :
48+
HasDerivWithinAt (f ^ n)
49+
(βˆ‘ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) s x := h.fun_pow' n
50+
51+
theorem HasDerivAt.fun_pow' (h : HasDerivAt f f' x) (n : β„•) :
52+
HasDerivAt (fun x ↦ f x ^ n)
53+
(βˆ‘ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x := by
54+
simpa using h.hasFDerivAt.pow' n |>.hasDerivAt
55+
56+
theorem HasDerivAt.pow' (h : HasDerivAt f f' x) (n : β„•) :
57+
HasDerivAt (f ^ n)
58+
(βˆ‘ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x := h.fun_pow' n
59+
60+
@[simp low]
61+
theorem derivWithin_fun_pow' (h : DifferentiableWithinAt π•œ f s x) (n : β„•) :
62+
derivWithin (fun x => f x ^ n) s x =
63+
βˆ‘ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i := by
64+
by_cases hsx : UniqueDiffWithinAt π•œ s x
65+
Β· exact (h.hasDerivWithinAt.pow' n).derivWithin hsx
66+
Β· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
2567

26-
/-! ### Derivative of `x ↦ x^n` for `n : β„•` -/
68+
@[simp low]
69+
theorem derivWithin_pow' (h : DifferentiableWithinAt π•œ f s x) (n : β„•) :
70+
derivWithin (f ^ n) s x =
71+
βˆ‘ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i :=
72+
derivWithin_fun_pow' h n
2773

28-
variable {c : π•œ β†’ π•œ} {c' : π•œ}
29-
variable (n : β„•)
74+
@[simp low]
75+
theorem deriv_fun_pow' (h : DifferentiableAt π•œ f x) (n : β„•) :
76+
deriv (fun x => f x ^ n) x = βˆ‘ i ∈ Finset.range n, f x ^ (n.pred - i) * deriv f x * f x ^ i :=
77+
(h.hasDerivAt.pow' n).deriv
3078

31-
theorem hasStrictDerivAt_pow :
32-
βˆ€ (n : β„•) (x : π•œ), HasStrictDerivAt (fun x : π•œ ↦ x ^ n) ((n : π•œ) * x ^ (n - 1)) x
33-
| 0, x => by simp [hasStrictDerivAt_const]
34-
| 1, x => by simpa using hasStrictDerivAt_id x
35-
| n + 1 + 1, x => by
36-
simpa [pow_succ, add_mul, mul_assoc] using
37-
(hasStrictDerivAt_pow (n + 1) x).fun_mul (hasStrictDerivAt_id x)
79+
@[simp low]
80+
theorem deriv_pow' (h : DifferentiableAt π•œ f x) (n : β„•) :
81+
deriv (f ^ n) x = βˆ‘ i ∈ Finset.range n, f x ^ (n.pred - i) * deriv f x * f x ^ i :=
82+
deriv_fun_pow' h n
3883

39-
theorem hasDerivAt_pow (n : β„•) (x : π•œ) :
40-
HasDerivAt (fun x : π•œ => x ^ n) ((n : π•œ) * x ^ (n - 1)) x :=
41-
(hasStrictDerivAt_pow n x).hasDerivAt
84+
end NormedRing
4285

43-
theorem hasDerivWithinAt_pow (n : β„•) (x : π•œ) (s : Set π•œ) :
44-
HasDerivWithinAt (fun x : π•œ => x ^ n) ((n : π•œ) * x ^ (n - 1)) s x :=
45-
(hasDerivAt_pow n x).hasDerivWithinAt
86+
section NormedCommRing
87+
variable [NontriviallyNormedField π•œ] [NormedCommRing 𝔸]
88+
variable [NormedAlgebra π•œ 𝔸] {f : π•œ β†’ 𝔸} {f' : 𝔸} {x : π•œ} {s : Set π•œ}
4689

47-
theorem differentiableAt_pow : DifferentiableAt π•œ (fun x : π•œ => x ^ n) x :=
48-
(hasDerivAt_pow n x).differentiableAt
90+
open scoped RightActions
4991

50-
theorem differentiableWithinAt_pow :
51-
DifferentiableWithinAt π•œ (fun x : π•œ => x ^ n) s x :=
52-
(differentiableAt_pow n).differentiableWithinAt
92+
nonrec theorem HasStrictDerivAt.fun_pow (h : HasStrictDerivAt f f' x) (n : β„•) :
93+
HasStrictDerivAt (fun x ↦ f x ^ n) (n * f x ^ (n - 1) * f') x := by
94+
unfold HasStrictDerivAt
95+
convert h.pow n
96+
ext
97+
simp [mul_assoc]
5398

54-
theorem differentiable_pow : Differentiable π•œ fun x : π•œ => x ^ n := fun _ => differentiableAt_pow n
99+
nonrec theorem HasStrictDerivAt.pow (h : HasStrictDerivAt f f' x) (n : β„•) :
100+
HasStrictDerivAt (f ^ n) (n * f x ^ (n - 1) * f') x := h.fun_pow n
55101

56-
theorem differentiableOn_pow : DifferentiableOn π•œ (fun x : π•œ => x ^ n) s :=
57-
(differentiable_pow n).differentiableOn
102+
nonrec theorem HasDerivWithinAt.fun_pow (h : HasDerivWithinAt f f' s x) (n : β„•) :
103+
HasDerivWithinAt (fun x ↦ f x ^ n) (n * f x ^ (n - 1) * f') s x := by
104+
simpa using h.hasFDerivWithinAt.pow n |>.hasDerivWithinAt
58105

59-
theorem deriv_pow : deriv (fun x : π•œ => x ^ n) x = (n : π•œ) * x ^ (n - 1) :=
60-
(hasDerivAt_pow n x).deriv
106+
nonrec theorem HasDerivWithinAt.pow (h : HasDerivWithinAt f f' s x) (n : β„•) :
107+
HasDerivWithinAt (f ^ n) (n * f x ^ (n - 1) * f') s x := h.fun_pow n
61108

62-
@[simp]
63-
theorem deriv_pow' : (deriv fun x : π•œ => x ^ n) = fun x => (n : π•œ) * x ^ (n - 1) :=
64-
funext fun _ => deriv_pow n
109+
theorem HasDerivAt.fun_pow (h : HasDerivAt f f' x) (n : β„•) :
110+
HasDerivAt (fun x ↦ f x ^ n) (n * f x ^ (n - 1) * f') x := by
111+
simpa using h.hasFDerivAt.pow n |>.hasDerivAt
65112

66-
theorem derivWithin_pow (hxs : UniqueDiffWithinAt π•œ s x) :
67-
derivWithin (fun x : π•œ => x ^ n) s x = (n : π•œ) * x ^ (n - 1) :=
68-
(hasDerivWithinAt_pow n x s).derivWithin hxs
113+
theorem HasDerivAt.pow (h : HasDerivAt f f' x) (n : β„•) :
114+
HasDerivAt (f ^ n) (n * f x ^ (n - 1) * f') x := h.fun_pow n
69115

70-
theorem HasDerivWithinAt.fun_pow (hc : HasDerivWithinAt c c' s x) :
71-
HasDerivWithinAt (fun y => c y ^ n) ((n : π•œ) * c x ^ (n - 1) * c') s x :=
72-
(hasDerivAt_pow n (c x)).comp_hasDerivWithinAt x hc
116+
@[simp]
117+
theorem derivWithin_fun_pow (h : DifferentiableWithinAt π•œ f s x) (n : β„•) :
118+
derivWithin (fun x => f x ^ n) s x = n * f x ^ (n - 1) * derivWithin f s x := by
119+
by_cases hsx : UniqueDiffWithinAt π•œ s x
120+
Β· exact (h.hasDerivWithinAt.pow n).derivWithin hsx
121+
Β· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
73122

74-
theorem HasDerivWithinAt.pow (hc : HasDerivWithinAt c c' s x) :
75-
HasDerivWithinAt (c ^ n) ((n : π•œ) * c x ^ (n - 1) * c') s x :=
76-
(hasDerivAt_pow n (c x)).comp_hasDerivWithinAt x hc
123+
@[simp]
124+
theorem derivWithin_pow (h : DifferentiableWithinAt π•œ f s x) (n : β„•) :
125+
derivWithin (f ^ n) s x = n * f x ^ (n - 1) * derivWithin f s x :=
126+
derivWithin_fun_pow h n
77127

78-
theorem HasDerivAt.fun_pow (hc : HasDerivAt c c' x) :
79-
HasDerivAt (fun y => c y ^ n) ((n : π•œ) * c x ^ (n - 1) * c') x := by
80-
rw [← hasDerivWithinAt_univ] at *
81-
exact hc.pow n
128+
@[simp]
129+
theorem deriv_fun_pow (h : DifferentiableAt π•œ f x) (n : β„•) :
130+
deriv (fun x => f x ^ n) x = n * f x ^ (n - 1) * deriv f x :=
131+
(h.hasDerivAt.pow n).deriv
82132

83-
theorem HasDerivAt.pow (hc : HasDerivAt c c' x) :
84-
HasDerivAt (c ^ n) ((n : π•œ) * c x ^ (n - 1) * c') x :=
85-
hc.fun_pow _
133+
@[simp]
134+
theorem deriv_pow (h : DifferentiableAt π•œ f x) (n : β„•) :
135+
deriv (f ^ n) x = n * f x ^ (n - 1) * deriv f x := deriv_fun_pow h n
86136

87-
theorem derivWithin_fun_pow' (hc : DifferentiableWithinAt π•œ c s x) :
88-
derivWithin (fun x => c x ^ n) s x = (n : π•œ) * c x ^ (n - 1) * derivWithin c s x := by
89-
by_cases hsx : UniqueDiffWithinAt π•œ s x
90-
Β· exact (hc.hasDerivWithinAt.pow n).derivWithin hsx
91-
Β· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
137+
end NormedCommRing
92138

93-
theorem derivWithin_pow' (hc : DifferentiableWithinAt π•œ c s x) :
94-
derivWithin (c ^ n) s x = (n : π•œ) * c x ^ (n - 1) * derivWithin c s x :=
95-
derivWithin_fun_pow' _ hc
139+
section NontriviallyNormedField
140+
variable [NontriviallyNormedField π•œ] {x : π•œ} {s : Set π•œ} {c : π•œ β†’ π•œ}
96141

97-
@[simp]
98-
theorem deriv_fun_pow'' (hc : DifferentiableAt π•œ c x) :
142+
@[deprecated deriv_fun_pow (since := "2025-07-16")]
143+
theorem deriv_fun_pow'' {c : π•œ β†’ π•œ} (n : β„•) (hc : DifferentiableAt π•œ c x) :
99144
deriv (fun x => c x ^ n) x = (n : π•œ) * c x ^ (n - 1) * deriv c x :=
100-
(hc.hasDerivAt.pow n).deriv
145+
deriv_fun_pow hc n
101146

102-
@[simp]
103-
theorem deriv_pow'' (hc : DifferentiableAt π•œ c x) :
147+
@[deprecated deriv_pow (since := "2025-07-16")]
148+
theorem deriv_pow'' {c : π•œ β†’ π•œ} (n : β„•) (hc : DifferentiableAt π•œ c x) :
104149
deriv (c ^ n) x = (n : π•œ) * c x ^ (n - 1) * deriv c x :=
105-
(hc.hasDerivAt.pow n).deriv
150+
deriv_pow hc n
151+
152+
theorem hasStrictDerivAt_pow (n : β„•) (x : π•œ) :
153+
HasStrictDerivAt (fun x : π•œ ↦ x ^ n) (n * x ^ (n - 1)) x := by
154+
simpa using (hasStrictDerivAt_id x).pow n
155+
156+
theorem hasDerivWithinAt_pow (n : β„•) (x : π•œ) :
157+
HasDerivWithinAt (fun x : π•œ ↦ x ^ n) (n * x ^ (n - 1)) s x := by
158+
simpa using (hasDerivWithinAt_id x s).pow n
159+
160+
theorem hasDerivAt_pow (n : β„•) (x : π•œ) :
161+
HasDerivAt (fun x : π•œ => x ^ n) ((n : π•œ) * x ^ (n - 1)) x := by
162+
simpa using (hasStrictDerivAt_pow n x).hasDerivAt
163+
164+
theorem derivWithin_pow_field (h : UniqueDiffWithinAt π•œ s x) (n : β„•) :
165+
derivWithin (fun x => x ^ n) s x = (n : π•œ) * x ^ (n - 1) := by
166+
rw [derivWithin_fun_pow (differentiableWithinAt_id' (s := s)) n, derivWithin_id' _ _ h, mul_one]
167+
168+
theorem deriv_pow_field (n : β„•) : deriv (fun x => x ^ n) x = (n : π•œ) * x ^ (n - 1) := by
169+
simp
170+
171+
end NontriviallyNormedField

β€ŽMathlib/Analysis/Calculus/FDeriv/Mul.leanβ€Ž

Lines changed: 0 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -502,44 +502,6 @@ theorem Differentiable.fun_mul (ha : Differentiable π•œ a) (hb : Differentiable
502502
theorem Differentiable.mul (ha : Differentiable π•œ a) (hb : Differentiable π•œ b) :
503503
Differentiable π•œ (a * b) := fun x => (ha x).mul (hb x)
504504

505-
@[fun_prop]
506-
theorem DifferentiableWithinAt.fun_pow (ha : DifferentiableWithinAt π•œ a s x) :
507-
βˆ€ n : β„•, DifferentiableWithinAt π•œ (fun x => a x ^ n) s x
508-
| 0 => by simp only [pow_zero, differentiableWithinAt_const]
509-
| n + 1 => by simp only [pow_succ', DifferentiableWithinAt.fun_pow ha n, ha.fun_mul]
510-
511-
@[fun_prop]
512-
theorem DifferentiableWithinAt.pow (ha : DifferentiableWithinAt π•œ a s x) :
513-
βˆ€ n : β„•, DifferentiableWithinAt π•œ (a ^ n) s x :=
514-
ha.fun_pow
515-
516-
@[simp, fun_prop]
517-
theorem DifferentiableAt.fun_pow (ha : DifferentiableAt π•œ a x) (n : β„•) :
518-
DifferentiableAt π•œ (fun x => a x ^ n) x :=
519-
differentiableWithinAt_univ.mp <| ha.differentiableWithinAt.pow n
520-
521-
@[simp, fun_prop]
522-
theorem DifferentiableAt.pow (ha : DifferentiableAt π•œ a x) (n : β„•) :
523-
DifferentiableAt π•œ (a ^ n) x :=
524-
differentiableWithinAt_univ.mp <| ha.differentiableWithinAt.pow n
525-
526-
@[fun_prop]
527-
theorem DifferentiableOn.fun_pow (ha : DifferentiableOn π•œ a s) (n : β„•) :
528-
DifferentiableOn π•œ (fun x => a x ^ n) s := fun x h => (ha x h).pow n
529-
530-
@[fun_prop]
531-
theorem DifferentiableOn.pow (ha : DifferentiableOn π•œ a s) (n : β„•) :
532-
DifferentiableOn π•œ (a ^ n) s := fun x h => (ha x h).pow n
533-
534-
@[simp, fun_prop]
535-
theorem Differentiable.fun_pow (ha : Differentiable π•œ a) (n : β„•) :
536-
Differentiable π•œ fun x => a x ^ n :=
537-
fun x => (ha x).pow n
538-
539-
@[simp, fun_prop]
540-
theorem Differentiable.pow (ha : Differentiable π•œ a) (n : β„•) : Differentiable π•œ (a ^ n) :=
541-
fun x => (ha x).pow n
542-
543505
theorem fderivWithin_fun_mul' (hxs : UniqueDiffWithinAt π•œ s x) (ha : DifferentiableWithinAt π•œ a s x)
544506
(hb : DifferentiableWithinAt π•œ b s x) :
545507
fderivWithin π•œ (fun y => a y * b y) s x =

0 commit comments

Comments
Β (0)