Analyticity of Harmonic Functions

If f : ℂ → ℝ is harmonic at x, we show that ∂f/∂1 - I • ∂f/∂I is complex-analytic at x. If f is harmonic on an open ball, then it is the real part of a function F : ℂ → ℂ that is holomorphic on the ball. This implies in particular that harmonic functions are real-analytic.

theorem HarmonicAt.differentiableAt_complex_partial {f : ℂ → ℝ} {x : ℂ} (hf : InnerProductSpace.HarmonicAt f x) : DifferentiableAt ℂ (fun (z : ℂ) => ↑((fderiv ℝ f z) 1) - Complex.I * ↑((fderiv ℝ f z) Complex.I)) x

If f : ℂ → ℝ is harmonic at x, then ∂f/∂1 - I • ∂f/∂I is complex differentiable at x.

theorem HarmonicAt.analyticAt_complex_partial {f : ℂ → ℝ} {x : ℂ} (hf : InnerProductSpace.HarmonicAt f x) : AnalyticAt ℂ (fun (z : ℂ) => ↑((fderiv ℝ f z) 1) - Complex.I * ↑((fderiv ℝ f z) Complex.I)) x

If f : ℂ → ℝ is harmonic at x, then ∂f/∂1 - I • ∂f/∂I is complex analytic at x.

theorem harmonic_is_realOfHolomorphic {f : ℂ → ℝ} {z : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicOnNhd f (Metric.ball z R)) : ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (Metric.ball z R) ∧ Set.EqOn (fun (z : ℂ) => (F z).re) f (Metric.ball z R)

theorem HarmonicAt.analyticAt {f : ℂ → ℝ} {x : ℂ} (hf : InnerProductSpace.HarmonicAt f x) : AnalyticAt ℝ f x