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 InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq {f : ℂ → ℝ} {z : ℂ} {R : ℝ} (hf : 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)

@[deprecated InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq (since := "2026-03-03")]

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)

Alias of InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq.

theorem InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq {f : ℂ → ℝ} (hf : HarmonicOnNhd f Set.univ) : ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F Set.univ ∧ (fun (z : ℂ) => (F z).re) = f

If a function f : ℂ → ℝ is harmonic, then f is the real part of a holomorphic function.

@[deprecated InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq (since := "2026-03-03")]

theorem InnerProductSpace.harmonic_is_realOfHolomorphic_univ {f : ℂ → ℝ} (hf : HarmonicOnNhd f Set.univ) : ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F Set.univ ∧ (fun (z : ℂ) => (F z).re) = f

Alias of InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq.

---

If a function f : ℂ → ℝ is harmonic, then f is the real part of a holomorphic function.

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