Commit 2025-07-27 09:27 6edce77c
View on Github →feat: establish examples of harmonic functions (#26844)
If f : ℂ → F is complex-differentiable, then show that 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.
This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis.