Commit 2026-02-25 19:11 ec467177

View on Github →

feat: introduce HarmonicContOnCl (#35564) Define a predicate HarmonicContOnCl that expresses a standard assumption of harmonic analysis: a function is harmonic on a domain and is continuous on its closure.

Estimated changes

Modified Mathlib.lean

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

added theorem InnerProductSpace.HarmonicAt.neg

added theorem InnerProductSpace.HarmonicAt.sub

added theorem InnerProductSpace.HarmonicOnNhd.continuousOn

added theorem InnerProductSpace.HarmonicOnNhd.neg

added theorem InnerProductSpace.HarmonicOnNhd.sub

added theorem InnerProductSpace.harmonicAt_const

added theorem InnerProductSpace.harmonicOnNhd_const

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

added theorem InnerProductSpace.HarmonicContOnCl.add

added theorem InnerProductSpace.HarmonicContOnCl.add_const

added theorem InnerProductSpace.HarmonicContOnCl.const_add

added theorem InnerProductSpace.HarmonicContOnCl.const_smul

added theorem InnerProductSpace.HarmonicContOnCl.const_sub

added theorem InnerProductSpace.HarmonicContOnCl.contDiffAt

added theorem InnerProductSpace.HarmonicContOnCl.continuousOn_ball

added theorem InnerProductSpace.HarmonicContOnCl.differentiableAt

added theorem InnerProductSpace.HarmonicContOnCl.mk_ball

added theorem InnerProductSpace.HarmonicContOnCl.mono

added theorem InnerProductSpace.HarmonicContOnCl.neg

added theorem InnerProductSpace.HarmonicContOnCl.sub

added theorem InnerProductSpace.HarmonicContOnCl.sub_const

added structure InnerProductSpace.HarmonicContOnCl

added theorem InnerProductSpace.HarmonicOnNhd.harmonicContOnCl

added theorem InnerProductSpace.IsClosed.harmonicContOnCl_iff

added theorem InnerProductSpace.harmonicContOnCl_const

Modified Mathlib/Analysis/InnerProductSpace/Laplacian.lean

added theorem ContDiffAt.laplacianWithin_sub_nhdsWithin

added theorem ContDiffAt.laplacian_sub

added theorem ContDiffAt.laplacian_sub_nhds

added theorem ContDiffWithinAt.laplacianWithin_sub

added theorem InnerProductSpace.laplacianWithin_neg

added theorem InnerProductSpace.laplacian_const

added theorem InnerProductSpace.laplacian_neg