Centered Classes Lie In The Diffusion Image Closure

This formalizes the mean-zero density statement recorded as Lemma A.6 of Letwin (arXiv:2607.24164v1), with the reviewed relation recorded as partial.

Let $V$ be finite-dimensional, let $m$ be an additive Haar measure, let $\nu$ be log-concave with

where $U\in C^1(V)$. If $g\in L^2(\nu)$ has zero mean,

then $g$ belongs to the closure in $L^2(\nu)$ of the literal images of smooth compactly supported functions under the diffusion operator compactSmoothDiffusionImage:

The conclusion is a closure statement for every mean-zero $L^2$ class; it does not state the Brascamp–Lieb inequality itself.

Original Lean declaration header

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

theorem centered_mem_closure_compactSmoothDiffusionImage
    {ν : ProbabilityMeasure V} (m : Measure V) [m.IsAddHaarMeasure]
    (hν : FunctionalInequalities.KLS.LogConcave ν) {U : V → ℝ}
    (hνU : (ν : Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 1 U)
    (g : Lp ℝ 2 (ν : Measure V)) (hg : L2.mean ν g = 0) :
    g ∈ closure (compactSmoothDiffusionImage hU)

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Range.

Definition modules: L2/MeanVariance, Probability/LogConcave.

Supporting theorems: mem_closure_range_of_inner_eq_zero, eq_const_mean_of_closedWeightedOperator_eq_zero, exists_seq_smooth_tendsto_adjointComp_of_localRegularity, interior_support_nonempty_of_eq_tilted, toLp_mul_mem_closedWeightedOperator_domain_of_orthogonal.

Source excerpt, lines 45–50 · Frozen source 408915f.