Construction of Harmonic Functions #
This file constructs examples of harmonic functions.
If f : ℂ → F is complex-differentiable, then f is harmonic. If F = ℂ, then so is its real
part, imaginary part, and complex conjugate. If f has no zero, then log ‖f‖ is harmonic.
Harmonicity of Analytic Functions on the Complex Plane #
theorem
ContDiffAt.harmonicAt
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{f : ℂ → F}
{x : ℂ}
(h : ContDiffAt ℂ 2 f x)
:
Continuously complex-differentiable functions on ℂ are harmonic.
theorem
AnalyticAt.harmonicAt
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{f : ℂ → F}
{x : ℂ}
[CompleteSpace F]
(h : AnalyticAt ℂ f x)
:
Analytic functions on ℂ are harmonic.
theorem
AnalyticAt.harmonicAt_re
{x : ℂ}
{f : ℂ → ℂ}
(h : AnalyticAt ℂ f x)
:
InnerProductSpace.HarmonicAt (fun (z : ℂ) => (f z).re) x
If f : ℂ → ℂ is complex-analytic, then its real part is harmonic.
theorem
AnalyticAt.harmonicAt_im
{x : ℂ}
{f : ℂ → ℂ}
(h : AnalyticAt ℂ f x)
:
InnerProductSpace.HarmonicAt (fun (z : ℂ) => (f z).im) x
If f : ℂ → ℂ is complex-analytic, then its imaginary part is harmonic.
theorem
AnalyticAt.harmonicAt_conj
{x : ℂ}
{f : ℂ → ℂ}
(h : AnalyticAt ℂ f x)
:
InnerProductSpace.HarmonicAt ((starRingEnd (ℂ → ℂ)) f) x
If f : ℂ → ℂ is complex-analytic, then its complex conjugate is harmonic.
Harmonicity of log ‖analytic‖ #
theorem
AnalyticAt.harmonicAt_log_norm
{f : ℂ → ℂ}
{z : ℂ}
(h₁f : AnalyticAt ℂ f z)
(h₂f : f z ≠ 0)
:
InnerProductSpace.HarmonicAt (fun (x : ℂ) => Real.log ‖f x‖) z
If f : ℂ → ℂ is complex-analytic without zero, then log ‖f‖ is harmonic.