English
For a function f: ℂ → E and a point c ∈ ℂ, f is analytic at c if and only if f is differentiable at every point in a neighborhood of c (i.e., differentiable eventually near c).
Русский
Для функции f: ℂ → E и точки c ∈ ℂ аналитичность в точке c эквивалентна тому, что f дифференцируема во всех точках окрестности c (то есть в окрестности c имеется предельная дифференцируемость).
LaTeX
$$$$ AnalyticAt_{\\mathbb{C}}(f, c) \\;\Longleftrightarrow\\; \\forall^\\infty z \\in \\mathcal{N}(c): DifferentiableAt_{\\mathbb{C}}(f, z). $$$$
Lean4
/-- `f : ℂ → E` is analytic at `z` iff it's differentiable near `z` -/
theorem analyticAt_iff_eventually_differentiableAt {f : ℂ → E} {c : ℂ} :
AnalyticAt ℂ f c ↔ ∀ᶠ z in 𝓝 c, DifferentiableAt ℂ f z :=
by
constructor
· intro fa
filter_upwards [fa.eventually_analyticAt]
apply AnalyticAt.differentiableAt
· intro d
rcases _root_.eventually_nhds_iff.mp d with ⟨s, d, o, m⟩
have h : AnalyticOnNhd ℂ f s := by
refine DifferentiableOn.analyticOnNhd ?_ o
intro z m
exact (d z m).differentiableWithinAt
exact h _ m
