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)
:
If f : ℂ → ℝ is harmonic at x, then ∂f/∂1 - I • ∂f/∂I is complex differentiable 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)
:
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)
:
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