English
If a function f: ℂ → ℝ is harmonic at x, then f is analytic at x as a real-valued function.
Русский
Если f: ℂ → ℝ гармонична в точке x, то она аналитична в точке x как функция в вещественном смысле.
LaTeX
$$$\\text{If } f: \\mathbb{C} \\to \\mathbb{R} \\text{ is harmonic at } x, \\text{ then } f \\text{ is analytic at } x$.$$
Lean4
theorem analyticAt (hf : HarmonicAt f x) : AnalyticAt ℝ f x :=
by
obtain ⟨ε, h₁ε, h₂ε⟩ := isOpen_iff.1 (isOpen_setOf_harmonicAt (f := f)) x hf
obtain ⟨F, h₁F, h₂F⟩ := harmonic_is_realOfHolomorphic (fun _ hy ↦ h₂ε hy)
rw [analyticAt_congr (Filter.eventually_of_mem (ball_mem_nhds x h₁ε) (fun y hy ↦ h₂F.symm hy))]
exact (reCLM.analyticAt (F x)).comp (h₁F x (mem_ball_self h₁ε)).restrictScalars
