Weak Equation For A Tilted Density Class

Proved

FunctionalInequalities.KLS.LogConcave.integral_laplacian_mul_tiltedDensity_mul_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This lemma converts an operator orthogonality relation into a Haar-measure weak equation.

Let $V$ be finite-dimensional, let $m$ be an additive Haar measure, let $\nu$ be log-concave with nonempty interior support, and let $U\in C^1(V)$ satisfy $\nu=m.\operatorname{tilted}(-U)$ . Let $u\in L^2(\nu)$ be orthogonal to $(A+1)C_c^\infty(V)$ , meaning

\langle Af,u\rangle+\langle f,u\rangle=0

for every smooth compactly supported $f$ , with $A=\overline{T}^{\dagger}\overline{T}$ . Then every such $f$ satisfies

\int_V (\Delta f)(x)\,\rho(x)u(x)\,dm(x) = \int_V \left\langle\nabla f(x),\rho(x)u(x)\nabla U(x)\right\rangle\,dm(x) +\int_V f(x)\rho(x)u(x)\,dm(x),

where $\rho=\texttt{tiltedDensity}(m,U)$ . This is the divergence-form equation used in the interior-regularity argument.

Original Lean declaration header

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

private theorem integral_laplacian_mul_tiltedDensity_mul
    (hνU : (ν : Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 1 U) (u : Lp ℝ 2 (ν : Measure V))
    (horth : ∀ (f : V → ℝ) (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f),
      ⟪(adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)
          ⟨_, hν.toLp_mem_adjointComp_domain m hi hνU hU hf hfc⟩ : Lp ℝ 2 (ν : Measure V)), u⟫ +
        ⟪((memLp_of_contDiff_hasCompactSupport ν hf hfc).toLp f : Lp ℝ 2 (ν : Measure V)), u⟫ = 0)
    {f : V → ℝ} (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f) :
    ∫ x, Laplacian.laplacian f x * (tiltedDensity m U x * u x) ∂m =
      ∫ x, ⟪gradient f x, (tiltedDensity m U x * u x) • gradient U x⟫ ∂m +
        ∫ x, f x * (tiltedDensity m U x * u x) ∂m

Module navigation

Module: KLS/LogConcave/HeatSemigroup/InteriorRegularity.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, KLS/LogConcave/HeatSemigroup/Generator, Analysis/Semigroup/AdjointComp, Probability/LogConcave, Energy/WeightedGradient/Core.

Previous: integral_laplacian_mul_convolution_eq · Next: toLp_mul_mem_closedWeightedOperator_domain_of_orthogonal.

Source excerpt, lines 467–476 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_InteriorRegularity

open MeasureTheory Filter Topology Metric InnerProductSpace
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open scoped ContDiff RealInnerProductSpace Convolution ENNReal
open FunctionalInequalities.Energy FunctionalInequalities.Energy.WeightedGradient
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
variable {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] {U : V → ℝ}
variable (hν : FunctionalInequalities.KLS.LogConcave ν) (hi : (interior (ν : MeasureTheory.Measure V).support).Nonempty)

Formal statement


 theorem FunctionalInequalities.KLS.LogConcave.integral_laplacian_mul_tiltedDensity_mul_readable
    (hνU : (ν : Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 1 U) (u : Lp ℝ 2 (ν : Measure V))
    (horth : ∀ (f : V → ℝ) (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f),
      ⟪(adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)
          ⟨_, hν.toLp_mem_adjointComp_domain m hi hνU hU hf hfc⟩ : Lp ℝ 2 (ν : Measure V)), u⟫ +
        ⟪((memLp_of_contDiff_hasCompactSupport ν hf hfc).toLp f : Lp ℝ 2 (ν : Measure V)), u⟫ = 0)
    {f : V → ℝ} (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f) :
    ∫ x, Laplacian.laplacian f x * (FunctionalInequalities.KLS.LogConcave.tiltedDensity m U x * u x) ∂m =
      ∫ x, ⟪gradient f x, (FunctionalInequalities.KLS.LogConcave.tiltedDensity m U x * u x) • gradient U x⟫ ∂m +
        ∫ x, f x * (FunctionalInequalities.KLS.LogConcave.tiltedDensity m U x * u x) ∂m := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HeatSemigroup/InteriorRegularity.lean#L463-L525 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HeatSemigroup.InteriorRegularity`, declaration `_private.FunctionalInequalities.KLS.LogConcave.HeatSemigroup.InteriorRegularity.0.FunctionalInequalities.KLS.LogConcave.integral_laplacian_mul_tiltedDensity_mul`; the repository is private at upload time).

View graph