English
If f: ℂ → ℝ is harmonic at x, then g(z) = ∂f/∂1 − i·∂f/∂I is complex analytic at x.
Русский
Если f: ℂ → ℝ гармонична в точке x, то g(z) = ∂f/∂1 − i·∂f/∂I аналитична в окрестности x.
LaTeX
$$$\\text{If } f \\colon \\mathbb{C} \\to \\mathbb{R} \\text{ is harmonic at } x, \\text{ then } g(z) = \\frac{∂f}{∂1}(z) - i \\frac{∂f}{∂I}(z) \\text{ is analytic at } x.$$$
Lean4
/-- If `f : ℂ → ℝ` is harmonic at `x`, then `∂f/∂1 - I • ∂f/∂I` is complex analytic at `x`.
-/
theorem analyticAt_complex_partial (hf : HarmonicAt f x) :
AnalyticAt ℂ (fun z ↦ fderiv ℝ f z 1 - I * fderiv ℝ f z I) x :=
DifferentiableOn.analyticAt (s := {x | HarmonicAt f x})
(fun _ hy ↦ (HarmonicAt.differentiableAt_complex_partial hy).differentiableWithinAt)
((isOpen_setOf_harmonicAt f).mem_nhds hf)
/-
If a function `f : ℂ → ℝ` is harmonic on an open ball, then `f` is the real part of a function
`F : ℂ → ℂ` that is holomorphic on the ball.
-/
