Commit 2026-03-02 19:44 dbb20211

View on Github →

feat: Liouville Theorem for harmonic functions (#35640) Implement Liouville's theorem for harmonic functions on the complex plane. This material is used in Project VD, formalizing Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/Harmonic/Analytic.lean

added theorem InnerProductSpace.harmonic_is_realOfHolomorphic_univ

Created Mathlib/Analysis/Complex/Harmonic/Liouville.lean

added theorem InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant

Modified Mathlib/Analysis/Complex/HasPrimitives.lean

added theorem Complex.IsConservativeOn.isExactOn_univ

added theorem Complex.IsExactOn.with_val_at

added theorem Differentiable.isExactOn_univ

Modified Mathlib/Analysis/InnerProductSpace/Harmonic/Basic.lean

added theorem InnerProductSpace.HarmonicOnNhd.contDiffOn

Modified Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

added theorem Complex.re_eq_re_of_cexp_eq_cexp