English
If a set s is a convex region and f is n-times continuously differentiable on s, then the map t ↦ taylorWithinEval f n s t x is continuous on s.
Русский
Если множество s выпукло и f обладает n‑кратной непрерывной дифференцируемостью на s, то t ↦ taylorWithinEval f n s t x непрерывно на s.
LaTeX
$$$\text{ContinuousOn}_{s}\bigl(\lambda t. taylorWithinEval(f,n,s,t,x)\bigr)$, при условии $\mathrm{UniqueDiffOn}(s)$ и $\mathrm{ContDiffOn}(f,n,s)$$$
Lean4
/-- If `f` is `n` times continuous differentiable on a set `s`, then the Taylor polynomial
`taylorWithinEval f n s x₀ x` is continuous in `x₀`. -/
theorem continuousOn_taylorWithinEval {f : ℝ → E} {x : ℝ} {n : ℕ} {s : Set ℝ} (hs : UniqueDiffOn ℝ s)
(hf : ContDiffOn ℝ n f s) : ContinuousOn (fun t => taylorWithinEval f n s t x) s :=
by
simp_rw [taylor_within_apply]
refine continuousOn_finset_sum (Finset.range (n + 1)) fun i hi => ?_
refine (continuousOn_const.mul ((continuousOn_const.sub continuousOn_id).pow _)).smul ?_
rw [contDiffOn_nat_iff_continuousOn_differentiableOn_deriv hs] at hf
simp only [Finset.mem_range] at hi
refine hf.1 i ?_
simp only [Nat.lt_succ_iff.mp hi]
