𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n) f s
⊢ ContinuousOn (fun t => ∑ k in Finset.range (n + 1), ((↑k !)⁻¹ * (x - t) ^ k) • iteratedDerivWithin k f s t) s
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n) f s
⊢ ContinuousOn (fun t => taylorWithinEval f n s t x) s
simp_rw [taylor_within_apply]
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n) f s
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ContinuousOn (fun t => ((↑i !)⁻¹ * (x - t) ^ i) • iteratedDerivWithin i f s t) s
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n) f s
⊢ ContinuousOn (fun t => ∑ k in Finset.range (n + 1), ((↑k !)⁻¹ * (x - t) ^ k) • iteratedDerivWithin k f s t) s
refine' continuousOn_finset_sum (Finset.range (n + 1)) fun i hi => _
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n) f s
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ContinuousOn (fun t => iteratedDerivWithin i f s t) s
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n) f s
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ContinuousOn (fun t => ((↑i !)⁻¹ * (x - t) ^ i) • iteratedDerivWithin i f s t) s
refine' (continuousOn_const.mul ((continuousOn_const.sub continuousOn_id).pow _)).smul _
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf :
  (∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (iteratedDerivWithin m f s) s) ∧
    ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ContinuousOn (fun t => iteratedDerivWithin i f s t) s
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n) f s
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ContinuousOn (fun t => iteratedDerivWithin i f s t) s
rw [contDiffOn_iff_continuousOn_differentiableOn_deriv hs] at hf
case intro
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
i : ℕ
hi : i ∈ Finset.range (n + 1)
hf_left : ∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (iteratedDerivWithin m f s) s
right✝ : ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s
⊢ ContinuousOn (fun t => iteratedDerivWithin i f s t) s
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf :
  (∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (iteratedDerivWithin m f s) s) ∧
    ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ContinuousOn (fun t => iteratedDerivWithin i f s t) s
cases' hf with hf_left
case intro
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
i : ℕ
hi : i ∈ Finset.range (n + 1)
right✝ : ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s
hf_left : ↑i ≤ ↑n → ContinuousOn (iteratedDerivWithin i f s) s
⊢ ContinuousOn (fun t => iteratedDerivWithin i f s t) s
case intro
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
i : ℕ
hi : i ∈ Finset.range (n + 1)
hf_left : ∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (iteratedDerivWithin m f s) s
right✝ : ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s
⊢ ContinuousOn (fun t => iteratedDerivWithin i f s t) s
specialize hf_left i
case intro
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
i : ℕ
right✝ : ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s
hf_left : ↑i ≤ ↑n → ContinuousOn (iteratedDerivWithin i f s) s
hi : i < n + 1
⊢ ContinuousOn (fun t => iteratedDerivWithin i f s t) s
case intro
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
i : ℕ
hi : i ∈ Finset.range (n + 1)
right✝ : ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s
hf_left : ↑i ≤ ↑n → ContinuousOn (iteratedDerivWithin i f s) s
⊢ ContinuousOn (fun t => iteratedDerivWithin i f s t) s
simp only [Finset.mem_range] at hi
case intro
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
i : ℕ
right✝ : ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s
hf_left : ↑i ≤ ↑n → ContinuousOn (iteratedDerivWithin i f s) s
hi : i < n + 1
⊢ ↑i ≤ ↑n
case intro
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
i : ℕ
right✝ : ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s
hf_left : ↑i ≤ ↑n → ContinuousOn (iteratedDerivWithin i f s) s
hi : i < n + 1
⊢ ContinuousOn (fun t => iteratedDerivWithin i f s t) s
refine' hf_left _
no goals
case intro
𝕜 : Type ?u.239708
E : Type u_1
F : Type ?u.239714
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
i : ℕ
right✝ : ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s
hf_left : ↑i ≤ ↑n → ContinuousOn (iteratedDerivWithin i f s) s
hi : i < n + 1
⊢ ↑i ≤ ↑n
simp only [WithTop.coe_le_coe, Nat.cast_le, Nat.lt_succ_iff.mp hi]