English
Let f be a function between normed spaces, defined on a set s with a point x. If the derivative structure of f is of class C^ω at x in the sense of ContDiffWithinAt, then f is analytic at x within s, and conversely, under suitable completeness conditions for the target space, ContDiffWithinAt 𝕜 ω f s x is equivalent to AnalyticWithinAt 𝕜 f s x.
Русский
Пусть f — функция между нормированными пространствами, определённая на sfетe s в точке x. Если поведение производной f относится к классу C^ω в точке x внутри s, то f аналитична в точке x на s, и наоборот, при подходящих условиях полноты пространства-образа ContDiffWithinAt 𝕜 ω f s x эквивалентно AnalyticWithinAt 𝕜 f s x.
LaTeX
$$$ ContDiffWithinAt 𝕜 \\omega f s x \\;\\iff\\; AnalyticWithinAt 𝕜 f s x$$
Lean4
theorem contDiffWithinAt_omega_iff_analyticWithinAt [CompleteSpace F] :
ContDiffWithinAt 𝕜 ω f s x ↔ AnalyticWithinAt 𝕜 f s x :=
by
refine ⟨fun h ↦ h.analyticWithinAt, fun h ↦ ?_⟩
obtain ⟨u, hu, p, hp, h'p⟩ := h.exists_hasFTaylorSeriesUpToOn ω
exact ⟨u, hu, p, hp.of_le le_top, fun i ↦ h'p i⟩
