Kernel Characterization for the Closed Unit Gradient

This statement characterizes the kernel of the closed unit gradient in the smooth tilted-measure setting.

Let $V$ be a finite-dimensional complete real inner product space with its Borel measurable structure and a second-countable topology. Assume:

1. $m$ is an additive Haar measure on $V$.
2. $\nu$ is a log-concave probability measure with $\operatorname{int}(\operatorname{supp}\nu)\ne\varnothing$.
3. $U:V\to\mathbb R$ is $C^2$ and $\nu=m.\operatorname{tilted}(-U)$, using Measure.tilted.

Let $T=$ KLS.LogConcave.closedWeightedOperator for the identity weight and $m$. For every $h\in D(T)$,

The mean and constant vector are L2.mean and L2.const. This identifies precisely the constant vectors in the gradient kernel and supports centered operator formulations.

Formalization Note The equality on the right is in $L^2(\nu)$, equivalently equality of representatives almost everywhere. No strict curvature lower bound or Poincaré bound is assumed.

Original Lean declaration header

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

theorem closedWeightedOperator_eq_zero_iff
    (h : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain) :
    hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi h = 0 ↔
      (h : Lp ℝ 2 (ν : Measure V)) = L2.const ν (L2.mean ν (h : Lp ℝ 2 (ν : Measure V)))

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Curvature.

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

Supporting theorems: closedWeightedOperator_one_eq_zero, eq_const_mean_of_closedWeightedOperator_eq_zero.

Previous: literatureConstant_le_inv_of_tendsto · Next: inner_center_eq_zero_of_closedWeightedOperator_eq_zero.

Source excerpt, lines 499–502 · Frozen source 408915f.