English
On a set with UniqueDiffOn, ContDiffOn 𝕜 ω f s is equivalent to AnalyticOn 𝕜 f s.
Русский
На множестве с уникальной дифференцируемостью ContDiffOn 𝕜 ω f s эквивалентно AnalyticOn 𝕜 f s.
LaTeX
$$$ContDiffOn\\ 𝕜\\ ω\\ f\\ s \\leftrightarrow AnalyticOn\\ 𝕜\\ f\\ s$$$
Lean4
theorem eventually_hasFTaylorSeriesUpToOn {f : E → F} {s : Set E} {a : E} (h : ContDiffWithinAt 𝕜 n f s a)
(hs : UniqueDiffOn 𝕜 s) (ha : a ∈ s) {m : ℕ} (hm : m ≤ n) :
∀ᶠ t in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn m f (ftaylorSeriesWithin 𝕜 f s) t :=
by
rcases h.contDiffOn' hm (by simp) with ⟨U, hUo, haU, hfU⟩
have : ∀ᶠ t in (𝓝[s] a).smallSets, t ⊆ s ∩ U :=
by
rw [eventually_smallSets_subset]
exact inter_mem_nhdsWithin _ <| hUo.mem_nhds haU
refine this.mono fun t ht ↦ .mono ?_ ht
rw [insert_eq_of_mem ha] at hfU
refine (hfU.ftaylorSeriesWithin (hs.inter hUo)).congr_series fun k hk x hx ↦ ?_
exact iteratedFDerivWithin_inter_open hUo hx.2
