The Closed Weighted Gradient Annihilates One

This statement asserts that the constant-one vector is annihilated by the closed weighted gradient.

Let $V$ be a finite-dimensional complete real inner product space with its Borel measurable structure and a second-countable topology. Let $m$ be an additive Haar measure, $B:V\to V$ a continuous linear map, and $\nu$ a log-concave probability measure with nonempty interior of its support. Let $T=$ KLS.LogConcave.closedWeightedOperator with weight $B$ and Haar measure $m$.

For the constant-one $L^2(\nu)$ vector $\mathbf1=$ L2.const ν 1, equipped with its certified membership in $D(T)$,

This supplies the constant-one kernel identity used in operator and semigroup formulations.

Formalization Note Domain membership is supplied by one_mem_domain_closedWeightedOperator. The equality is in the vector-valued $L^2$ target, hence concerns equivalence classes rather than a pointwise representative. No invertibility assumption on $B$ is imposed.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave. Shown in its original module context. Proof omitted.

theorem closedWeightedOperator_one_eq_zero (hν : LogConcave ν)
    (hi : (interior (ν : Measure V).support).Nonempty) :
    hν.closedWeightedOperator m B hi
        ⟨L2.const ν 1, one_mem_domain_closedWeightedOperator m B hν hi⟩ = 0

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Markov.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, Probability/LogConcave, L2/MeanVariance.

Source excerpt, lines 233–236 · Frozen source 408915f.