[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
[PROOFSTEP]
have : ∀ m : ℤ, 0 < m → HasStrictDerivAt (· ^ m) ((m : 𝕜) * x ^ (m - 1)) x := fun m hm ↦
  by
  lift m to ℕ using hm.le
  simp only [zpow_ofNat, Int.cast_ofNat]
  convert hasStrictDerivAt_pow m x using 2
  rw [← Int.ofNat_one, ← Int.ofNat_sub, zpow_ofNat]
  norm_cast at hm 
[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝¹ m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℤ
hm : 0 < m
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
[PROOFSTEP]
lift m to ℕ using hm.le
[GOAL]
case intro
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝¹ m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ HasStrictDerivAt (fun x => x ^ ↑m) (↑↑m * x ^ (↑m - 1)) x
[PROOFSTEP]
simp only [zpow_ofNat, Int.cast_ofNat]
[GOAL]
case intro
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝¹ m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (↑m - 1)) x
[PROOFSTEP]
convert hasStrictDerivAt_pow m x using 2
[GOAL]
case h.e'_7.h.e'_6
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝¹ m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ x ^ (↑m - 1) = x ^ (m - 1)
[PROOFSTEP]
rw [← Int.ofNat_one, ← Int.ofNat_sub, zpow_ofNat]
[GOAL]
case h.e'_7.h.e'_6
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝¹ m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ 1 ≤ m
[PROOFSTEP]
norm_cast at hm 
[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
[PROOFSTEP]
rcases lt_trichotomy m 0 with (hm | hm | hm)
[GOAL]
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
[PROOFSTEP]
have hx : x ≠ 0 := h.resolve_right hm.not_le
[GOAL]
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
[PROOFSTEP]
have := (hasStrictDerivAt_inv ?_).scomp _ (this (-m) (neg_pos.2 hm)) <;> [skip; exact zpow_ne_zero_of_ne_zero hx _]
[GOAL]
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
[PROOFSTEP]
have := (hasStrictDerivAt_inv ?_).scomp _ (this (-m) (neg_pos.2 hm))
[GOAL]
case inl.refine_2
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (Inv.inv ∘ fun x => x ^ (-m)) ((↑(-m) * x ^ (-m - 1)) • -((x ^ (-m)) ^ 2)⁻¹) x
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
[PROOFSTEP]
skip
[GOAL]
case inl.refine_1
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
⊢ x ^ (-m) ≠ 0
[PROOFSTEP]
exact zpow_ne_zero_of_ne_zero hx _
[GOAL]
case inl.refine_2
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (Inv.inv ∘ fun x => x ^ (-m)) ((↑(-m) * x ^ (-m - 1)) • -((x ^ (-m)) ^ 2)⁻¹) x
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
[PROOFSTEP]
simp only [(· ∘ ·), zpow_neg, one_div, inv_inv, smul_eq_mul] at this 
[GOAL]
case inl.refine_2
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_7
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹
[PROOFSTEP]
rw [sq, mul_inv, inv_inv, Int.cast_neg, neg_mul, neg_mul_neg, ← zpow_add₀ hx, mul_assoc, ← zpow_add₀ hx]
[GOAL]
case h.e'_7
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑m * x ^ (-m - 1 + (m + m))
[PROOFSTEP]
congr
[GOAL]
case h.e'_7.e_a.e_a
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ m - 1 = -m - 1 + (m + m)
[PROOFSTEP]
abel
[GOAL]
case h.e'_7.e_a.e_a
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x => x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ m - 1 = -m - 1 + (m + m)
[PROOFSTEP]
abel
[GOAL]
case inr.inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : m = 0
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
[PROOFSTEP]
simp only [hm, zpow_zero, Int.cast_zero, zero_mul, hasStrictDerivAt_const]
[GOAL]
case inr.inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
hm : 0 < m
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
[PROOFSTEP]
exact this m hm
[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
⊢ deriv (fun x => x ^ m) x = ↑m * x ^ (m - 1)
[PROOFSTEP]
by_cases H : x ≠ 0 ∨ 0 ≤ m
[GOAL]
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
H : x ≠ 0 ∨ 0 ≤ m
⊢ deriv (fun x => x ^ m) x = ↑m * x ^ (m - 1)
[PROOFSTEP]
exact (hasDerivAt_zpow m x H).deriv
[GOAL]
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ deriv (fun x => x ^ m) x = ↑m * x ^ (m - 1)
[PROOFSTEP]
rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_zpow.1 H)]
[GOAL]
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ 0 = ↑m * x ^ (m - 1)
[PROOFSTEP]
push_neg at H 
[GOAL]
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m✝ m : ℤ
x : 𝕜
H : x = 0 ∧ m < 0
⊢ 0 = ↑m * x ^ (m - 1)
[PROOFSTEP]
rcases H with ⟨rfl, hm⟩
[GOAL]
case neg.intro
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
m✝ m : ℤ
hm : m < 0
⊢ 0 = ↑m * 0 ^ (m - 1)
[PROOFSTEP]
rw [zero_zpow _ ((sub_one_lt _).trans hm).ne, mul_zero]
[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
m✝ m : ℤ
k : ℕ
⊢ (deriv^[k] fun x => x ^ m) = fun x => (∏ i in Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
[PROOFSTEP]
induction' k with k ihk
[GOAL]
case zero
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
m✝ m : ℤ
⊢ (deriv^[Nat.zero] fun x => x ^ m) = fun x => (∏ i in Finset.range Nat.zero, (↑m - ↑i)) * x ^ (m - ↑Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq, one_mul, Int.ofNat_zero, id, sub_zero, Finset.prod_range_zero, Function.iterate_zero]
[GOAL]
case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
m✝ m : ℤ
k : ℕ
ihk : (deriv^[k] fun x => x ^ m) = fun x => (∏ i in Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
⊢ (deriv^[Nat.succ k] fun x => x ^ m) = fun x => (∏ i in Finset.range (Nat.succ k), (↑m - ↑i)) * x ^ (m - ↑(Nat.succ k))
[PROOFSTEP]
simp only [Function.iterate_succ_apply', ihk, deriv_const_mul_field', deriv_zpow', Finset.prod_range_succ,
  Int.ofNat_succ, ← sub_sub, Int.cast_sub, Int.cast_ofNat, mul_assoc]
[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
⊢ deriv^[k] (fun x => x ^ n) x = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ (n - k)
[PROOFSTEP]
simp only [← zpow_ofNat, iter_deriv_zpow, Int.cast_ofNat]
[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
[PROOFSTEP]
cases' le_or_lt k n with hkn hnk
[GOAL]
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
hkn : k ≤ n
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
[PROOFSTEP]
rw [Int.ofNat_sub hkn]
[GOAL]
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
[PROOFSTEP]
have : (∏ i in Finset.range k, (n - i : 𝕜)) = 0 := Finset.prod_eq_zero (Finset.mem_range.2 hnk) (sub_self _)
[GOAL]
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
this : ∏ i in Finset.range k, (↑n - ↑i) = 0
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
[PROOFSTEP]
simp only [this, zero_mul]
[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
k : ℕ
x : 𝕜
⊢ deriv^[k] Inv.inv x = (∏ i in Finset.range k, (-1 - ↑i)) * x ^ (-1 - ↑k)
[PROOFSTEP]
simpa only [zpow_neg_one, Int.cast_neg, Int.cast_one] using iter_deriv_zpow (-1) x k
