case zero
𝕜 : Type ?u.230356
E : Type u_1
F : Type ?u.230362
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ taylorWithinEval f Nat.zero s x₀ x =
    ∑ k in Finset.range (Nat.zero + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀

case succ
𝕜 : Type ?u.230356
E : Type u_1
F : Type ?u.230362
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
k : ℕ
hk : taylorWithinEval f k s x₀ x = ∑ k in Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
⊢ taylorWithinEval f (Nat.succ k) s x₀ x =
    ∑ k in Finset.range (Nat.succ k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
𝕜 : Type ?u.230356
E : Type u_1
F : Type ?u.230362
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ taylorWithinEval f n s x₀ x = ∑ k in Finset.range (n + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
induction' n with k hk
case succ
𝕜 : Type ?u.230356
E : Type u_1
F : Type ?u.230362
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
k : ℕ
hk : taylorWithinEval f k s x₀ x = ∑ k in Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
⊢ ∑ k in Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀ +
      (((↑k + 1) * ↑k !)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀ =
    ∑ x_1 in Finset.range (k + 1), ((↑x_1 !)⁻¹ * (x - x₀) ^ x_1) • iteratedDerivWithin x_1 f s x₀ +
      ((↑(k + 1)!)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀
case succ
𝕜 : Type ?u.230356
E : Type u_1
F : Type ?u.230362
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
k : ℕ
hk : taylorWithinEval f k s x₀ x = ∑ k in Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
⊢ taylorWithinEval f (Nat.succ k) s x₀ x =
    ∑ k in Finset.range (Nat.succ k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
rw [taylorWithinEval_succ, Finset.sum_range_succ, hk]
no goals
case succ
𝕜 : Type ?u.230356
E : Type u_1
F : Type ?u.230362
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
k : ℕ
hk : taylorWithinEval f k s x₀ x = ∑ k in Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
⊢ ∑ k in Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀ +
      (((↑k + 1) * ↑k !)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀ =
    ∑ x_1 in Finset.range (k + 1), ((↑x_1 !)⁻¹ * (x - x₀) ^ x_1) • iteratedDerivWithin x_1 f s x₀ +
      ((↑(k + 1)!)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀
simp
no goals
case zero
𝕜 : Type ?u.230356
E : Type u_1
F : Type ?u.230362
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ taylorWithinEval f Nat.zero s x₀ x =
    ∑ k in Finset.range (Nat.zero + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
simp