English
If a function is meromorphic at x and analytic there, the analytic view implies a strong form of analyticity at x.
Русский
Если функция мероморфна в x и аналитична там, то аналитическое поведение приводит к аналитичности в окрестности x.
LaTeX
$$$\\text{MeromorphicAt}(f, x) \\land \\text{AnalyticAt}(f, x) \\Rightarrow \\text{AnalyticAt}(f, x)$$$
Lean4
/-- If a function is both meromorphic and continuous at a point, then it is analytic there. -/
protected theorem analyticAt {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) (h' : ContinuousAt f x) : AnalyticAt 𝕜 f x :=
by
cases ho : meromorphicOrderAt f x with
| top =>
/- If the order is infinite, then `f` vanishes on a pointed neighborhood of `x`. By continuity,
it also vanishes at `x`.-/
have : AnalyticAt 𝕜 (fun _ ↦ (0 : E)) x := analyticAt_const
apply this.congr
rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE continuousAt_const h']
filter_upwards [meromorphicOrderAt_eq_top_iff.1 ho] with y hy using by simp [hy]
| coe n =>
/- If the order is finite, then the order has to be nonnegative, as otherwise the norm of `f`
would tend to infinity at `x`. Then the local expression of `f` coming from its meromorphicity
shows that it coincides with an analytic function close to `x`, except maybe at `x`. By
continuity of `f`, the two functions also coincide at `x`. -/
rcases (meromorphicOrderAt_eq_int_iff h).1 ho with ⟨g, g_an, gx, hg⟩
have : 0 ≤ meromorphicOrderAt f x :=
by
apply (tendsto_nhds_iff_meromorphicOrderAt_nonneg h).1
exact ⟨f x, h'.continuousWithinAt.tendsto⟩
lift n to ℕ using by simpa [ho] using this
have A : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z :=
by
apply (ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) h').1
filter_upwards [hg] with z hz using by simpa using hz.symm
exact AnalyticAt.congr (by fun_prop) A
