Weighted Laplacian Vanishes Outside Closed Support

Proved

FunctionalInequalities.Analysis.BakryEmery.weightedLaplacian_eq_zero_of_notMem_tsupport_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement establishes locality of the weighted Laplacian weightedLaplacian.

Let $E$ be a complete finite-dimensional real inner-product space, let $U:E\to\mathbb R$ be arbitrary, let $f:E\to\mathbb R$ , and let $x\in E$ . If $x$ does not belong to the topological support of $f$ , then

\operatorname{weightedLaplacian}(U,f)(x)=0.

The conclusion is independent of the potential $U$ and expresses that the weighted Laplacian vanishes at every point outside the closed support of its argument.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.

theorem weightedLaplacian_eq_zero_of_notMem_tsupport (U : E → ℝ) {f : E → ℝ} {x : E}
    (hx : x ∉ tsupport f) : weightedLaplacian U f x = 0

Module navigation

Module: Analysis/BakryEmery/Laplacian.

Source excerpt, lines 51–52 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Laplacian

universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.weightedLaplacian_eq_zero_of_notMem_tsupport_readable (U : E → ℝ) {f : E → ℝ} {x : E}
    (hx : x ∉ tsupport f) : weightedLaplacian U f x = 0 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Laplacian.lean#L48-L64 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Laplacian`, declaration `FunctionalInequalities.Analysis.BakryEmery.weightedLaplacian_eq_zero_of_notMem_tsupport`; the repository is private at upload time).

View graph