[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


[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n f univ = iteratedDeriv n f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
⊢ iteratedDerivWithin n f univ x = iteratedDeriv n f x
[PROOFSTEP]
rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n f s =
    ↑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) ∘ iteratedFDerivWithin 𝕜 n f s
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
⊢ iteratedDerivWithin n f s x =
    (↑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) ∘ iteratedFDerivWithin 𝕜 n f s) x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedFDerivWithin 𝕜 n f s = ↑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDerivWithin n f s
[PROOFSTEP]
rw [iteratedDerivWithin_eq_equiv_comp, ← Function.comp.assoc, LinearIsometryEquiv.self_comp_symm, Function.left_id]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ ↑(iteratedFDerivWithin 𝕜 n f s x) m = (∏ i : Fin n, m i) • iteratedDerivWithin n f s x
[PROOFSTEP]
rw [iteratedDerivWithin_eq_iteratedFDerivWithin, ← ContinuousMultilinearMap.map_smul_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ ↑(iteratedFDerivWithin 𝕜 n f s x) m = ↑(iteratedFDerivWithin 𝕜 n f s x) fun i => m i • 1
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ ‖iteratedFDerivWithin 𝕜 n f s x‖ = ‖iteratedDerivWithin n f s x‖
[PROOFSTEP]
rw [iteratedDerivWithin_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin 0 f s = f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
⊢ iteratedDerivWithin 0 f s x = f x
[PROOFSTEP]
simp [iteratedDerivWithin]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
h : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin 1 f s x = derivWithin f s x
[PROOFSTEP]
simp only [iteratedDerivWithin, iteratedFDerivWithin_one_apply h]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
h : UniqueDiffWithinAt 𝕜 s x
⊢ ↑(fderivWithin 𝕜 f s x) 1 = derivWithin f s x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ContDiffOn 𝕜 n f s
[PROOFSTEP]
apply contDiffOn_of_continuousOn_differentiableOn
[GOAL]
case Hcont
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s
[PROOFSTEP]
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_continuousOn_iff]
[GOAL]
case Hdiff
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s
[PROOFSTEP]
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_iff]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
h : ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
⊢ ContDiffOn 𝕜 n f s
[PROOFSTEP]
apply contDiffOn_of_differentiableOn
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
h : ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
⊢ ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
[PROOFSTEP]
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_iff]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m ≤ n
hs : UniqueDiffOn 𝕜 s
⊢ ContinuousOn (iteratedDerivWithin m f s) s
[PROOFSTEP]
simpa only [iteratedDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_continuousOn_iff] using
  h.continuousOn_iteratedFDerivWithin hmn hs
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 (insert x s)
⊢ DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x
[PROOFSTEP]
simpa only [iteratedDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableWithinAt_iff] using
  h.differentiableWithinAt_iteratedFDerivWithin hmn hs
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ : 𝕜
n : ℕ∞
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : 𝕜
hx : x ∈ s
⊢ UniqueDiffOn 𝕜 (insert x s)
[PROOFSTEP]
rwa [insert_eq_of_mem hx]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 n f s ↔
    (∀ (m : ℕ), ↑m ≤ n → ContinuousOn (iteratedDerivWithin m f s) s) ∧
      ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
[PROOFSTEP]
simp only [contDiffOn_iff_continuousOn_differentiableOn hs, iteratedFDerivWithin_eq_equiv_comp,
  LinearIsometryEquiv.comp_continuousOn_iff, LinearIsometryEquiv.comp_differentiableOn_iff]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
[PROOFSTEP]
rw [iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left,
  iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_fderivWithin _ hxs, derivWithin]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ ↑(↑(ContinuousLinearMap.comp
              (↑(ContinuousLinearEquiv.mk (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).toLinearEquiv))
              (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x))
          1)
      (Fin.tail fun x => 1) =
    ↑(fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1
[PROOFSTEP]
change
  ((ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) ((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) :
        (Fin n → 𝕜) → F)
      fun i : Fin n => 1) =
    (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ (↑(ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) (↑(fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1)) fun i => 1) =
    ↑(fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedDerivWithin n f s x = (fun g => derivWithin g s)^[n] f x
[PROOFSTEP]
induction' n with n IH generalizing x
[GOAL]
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝¹ x✝ : 𝕜
hs : UniqueDiffOn 𝕜 s
hx✝ : x✝ ∈ s
x : 𝕜
hx : x ∈ s
⊢ iteratedDerivWithin Nat.zero f s x = (fun g => derivWithin g s)^[Nat.zero] f x
[PROOFSTEP]
simp
[GOAL]
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝¹ x✝ : 𝕜
hs : UniqueDiffOn 𝕜 s
hx✝ : x✝ ∈ s
n : ℕ
IH : ∀ {x : 𝕜}, x ∈ s → iteratedDerivWithin n f s x = (fun g => derivWithin g s)^[n] f x
x : 𝕜
hx : x ∈ s
⊢ iteratedDerivWithin (Nat.succ n) f s x = (fun g => derivWithin g s)^[Nat.succ n] f x
[PROOFSTEP]
rw [iteratedDerivWithin_succ (hs x hx), Function.iterate_succ']
[GOAL]
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝¹ x✝ : 𝕜
hs : UniqueDiffOn 𝕜 s
hx✝ : x✝ ∈ s
n : ℕ
IH : ∀ {x : 𝕜}, x ∈ s → iteratedDerivWithin n f s x = (fun g => derivWithin g s)^[n] f x
x : 𝕜
hx : x ∈ s
⊢ derivWithin (iteratedDerivWithin n f s) s x = ((fun g => derivWithin g s) ∘ (fun g => derivWithin g s)^[n]) f x
[PROOFSTEP]
exact derivWithin_congr (fun y hy => IH hy) (IH hx)
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hxs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedDerivWithin (n + 1) f s x = iteratedDerivWithin n (derivWithin f s) s x
[PROOFSTEP]
rw [iteratedDerivWithin_eq_iterate hxs hx, iteratedDerivWithin_eq_iterate hxs hx]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hxs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ (fun g => derivWithin g s)^[n + 1] f x = (fun g => derivWithin g s)^[n] (derivWithin f s) x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDeriv n f =
    ↑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) ∘ iteratedFDeriv 𝕜 n f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
⊢ iteratedDeriv n f x =
    (↑(LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F)) ∘ iteratedFDeriv 𝕜 n f) x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedFDeriv 𝕜 n f = ↑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDeriv n f
[PROOFSTEP]
rw [iteratedDeriv_eq_equiv_comp, ← Function.comp.assoc, LinearIsometryEquiv.self_comp_symm, Function.left_id]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ ↑(iteratedFDeriv 𝕜 n f x) m = (∏ i : Fin n, m i) • iteratedDeriv n f x
[PROOFSTEP]
rw [iteratedDeriv_eq_iteratedFDeriv, ← ContinuousMultilinearMap.map_smul_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ ↑(iteratedFDeriv 𝕜 n f x) m = ↑(iteratedFDeriv 𝕜 n f x) fun i => m i • 1
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ ‖iteratedFDeriv 𝕜 n f x‖ = ‖iteratedDeriv n f x‖
[PROOFSTEP]
rw [iteratedDeriv_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDeriv 0 f = f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
⊢ iteratedDeriv 0 f x = f x
[PROOFSTEP]
simp [iteratedDeriv]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDeriv 1 f = deriv f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
⊢ iteratedDeriv 1 f x = deriv f x
[PROOFSTEP]
simp [iteratedDeriv]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
⊢ ↑(fderiv 𝕜 f x) 1 = deriv f x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞
⊢ ContDiff 𝕜 n f ↔
    (∀ (m : ℕ), ↑m ≤ n → Continuous (iteratedDeriv m f)) ∧ ∀ (m : ℕ), ↑m < n → Differentiable 𝕜 (iteratedDeriv m f)
[PROOFSTEP]
simp only [contDiff_iff_continuous_differentiable, iteratedFDeriv_eq_equiv_comp,
  LinearIsometryEquiv.comp_continuous_iff, LinearIsometryEquiv.comp_differentiable_iff]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f)
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
⊢ iteratedDeriv (n + 1) f x = deriv (iteratedDeriv n f) x
[PROOFSTEP]
rw [← iteratedDerivWithin_univ, ← iteratedDerivWithin_univ, ← derivWithin_univ]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
⊢ iteratedDerivWithin (n + 1) f univ x = derivWithin (iteratedDerivWithin n f univ) univ x
[PROOFSTEP]
exact iteratedDerivWithin_succ uniqueDiffWithinAt_univ
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDeriv n f = deriv^[n] f
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
⊢ iteratedDeriv n f x = deriv^[n] f x
[PROOFSTEP]
rw [← iteratedDerivWithin_univ]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
⊢ iteratedDerivWithin n f univ x = deriv^[n] f x
[PROOFSTEP]
convert iteratedDerivWithin_eq_iterate uniqueDiffOn_univ (F := F) (mem_univ x)
[GOAL]
case h.e'_3.h.e'_1.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝¹ x : 𝕜
x✝ : 𝕜 → F
⊢ deriv x✝ = derivWithin x✝ univ
[PROOFSTEP]
simp [derivWithin_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)
[PROOFSTEP]
rw [iteratedDeriv_eq_iterate, iteratedDeriv_eq_iterate]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ deriv^[n + 1] f = deriv^[n] (deriv f)
[PROOFSTEP]
rfl