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.