Commit 2025-07-07 08:02 0a13a73d

View on Github →

feat: implement harmonic functions (#26721) Define harmonic functions on real, finite-dimensional, inner product spaces. 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.

Estimated changes

Modified Mathlib.lean

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

added theorem InnerProductSpace.HarmonicAt.add

added theorem InnerProductSpace.HarmonicAt.comp_CLM

added theorem InnerProductSpace.HarmonicAt.const_smul

added theorem InnerProductSpace.HarmonicAt.eventually

added def InnerProductSpace.HarmonicAt

added theorem InnerProductSpace.HarmonicOnNhd.add

added theorem InnerProductSpace.HarmonicOnNhd.comp_CLM

added theorem InnerProductSpace.HarmonicOnNhd.const_smul

added theorem InnerProductSpace.HarmonicOnNhd.mono

added def InnerProductSpace.HarmonicOnNhd

added theorem InnerProductSpace.harmonicAt_comp_CLE_iff

added theorem InnerProductSpace.harmonicAt_congr_nhds

added theorem InnerProductSpace.harmonicOnNhd_comp_CLE_iff

added theorem InnerProductSpace.isOpen_setOf_harmonicAt

Modified Mathlib/Analysis/InnerProductSpace/Laplacian.lean

added theorem ContDiffAt.laplacian_CLM_comp_left_nhds

added theorem ContDiffWithinAt.laplacianWithin_CLM_comp_left_nhds

added theorem InnerProductSpace.laplacianWithin_smul_nhds

added theorem InnerProductSpace.laplacian_smul_nhds