Generator identities for smooth compactly supported tests

Definition

KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Generator

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

functional-inequalitiesklartaglehec2022klskls-conjecturekls-modularlog-concavemodule-context

Assume a log-concave probability law satisfies $\nu=m.\operatorname{tilted}(-U)$ for a $C^1$ potential $U$ . The theorem integral_inner_gradient_eq states that for $f\in C_c^2(V)$ and $g\in C^1(V)$ , $\int\langle\nabla f,\nabla g\rangle\,d\nu=\int(-\mathcal L_Uf)g\,d\nu$ , where weightedLaplacian is $\mathcal L_U$ . For $f\in C_c^\infty(V)$ , the bundle establishes square-integrability of $\nabla f$ and $-\mathcal L_Uf$ , membership of $[f]$ in the domain of the closed gradient and its adjoint composition, and the corresponding weak identity; closedWeightedOperator_toLp_eq identifies the closed gradient of $[f]$ with $[\nabla f]$ .

Original module imports

import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Basic
import FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.Basic
import FunctionalInequalities.Analysis.Semigroup.AdjointClosure

Original declaration excerpt

Shown in the original module context.

theorem integral_inner_gradient_eq {f g : V → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f)
    (hg : ContDiff ℝ 1 g) :
    ∫ x, ⟪gradient f x, gradient g x⟫ ∂(ν : Measure V) =
      ∫ x, -weightedLaplacian U f x * g x ∂(ν : Measure V) := by
  rw [hνU]
  exact integral_inner_gradient_tilted m hU hf hfc hg

Module navigation

Direct project imports: KLS/LogConcave/HeatSemigroup/Basic, Analysis/BakryEmery/IntegrationByParts/Basic, Analysis/Semigroup/AdjointClosure.

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Generator · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Semigroup_AdjointClosure

noncomputable section
open MeasureTheory FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open scoped ContDiff LinearPMap RealInnerProductSpace
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
open Energy Energy.WeightedGradient
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
section Tilted
variable {ν : ProbabilityMeasure V} (m : Measure V) [m.IsAddHaarMeasure] {U : V → ℝ}
  (hνU : (ν : Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 1 U)
include hνU hU in
omit [SecondCountableTopology V] in
/-- **weighted integration by parts, weighted integration by parts for the law `ν = m.tilted (-U)`**: for a `C²` compactly
supported `f` and a `C¹` function `g`, `∫ ⟪∇f, ∇g⟫ dν = ∫ (-ℒf) g dν`. -/
theorem integral_inner_gradient_eq {f g : V → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f)
    (hg : ContDiff ℝ 1 g) :
    ∫ x, ⟪gradient f x, gradient g x⟫ ∂(ν : Measure V) =
      ∫ x, -weightedLaplacian U f x * g x ∂(ν : Measure V) := by
  rw [hνU]
  exact integral_inner_gradient_tilted m hU hf hfc hg
end Tilted
section Generator
variable {ν : ProbabilityMeasure V} (m : Measure V) [m.IsAddHaarMeasure] (hν : LogConcave ν)
  (hi : (interior (ν : Measure V).support).Nonempty) {U : V → ℝ}
  (hνU : (ν : Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 1 U)
omit [FiniteDimensional ℝ V] in
/-- The gradient of a smooth compactly supported function is square integrable for every
probability law. -/
theorem memLp_gradient_of_contDiff_hasCompactSupport {f : V → ℝ} (hf : ContDiff ℝ ∞ f)
    (hfc : HasCompactSupport f) : MemLp (gradient f) 2 (ν : Measure V) := by
  simpa only [apply_id] using
    (IsTest.of_contDiff_hasCompactSupport ν (ContinuousLinearMap.id ℝ V) hf hfc).memLp_apply
omit [SecondCountableTopology V] in
/-- `-ℒ f ∈ L²(ν)` for `f ∈ C_c^∞(V)` and a `C¹` potential: the integrability clause of the smooth-test generator identity. -/
theorem memLp_neg_weightedLaplacian (hU : ContDiff ℝ 1 U) {f : V → ℝ} (hf : ContDiff ℝ ∞ f)
    (hfc : HasCompactSupport f) :
    MemLp (fun x => -weightedLaplacian U f x) 2 (ν : Measure V) :=
  (memLp_weightedLaplacian hU (hf.of_le (WithTop.coe_le_coe.mpr le_top)) hfc 2).neg
/-- The class of a smooth compactly supported function lies in the domain of the closed
unit-weight gradient. -/
theorem toLp_mem_closedWeightedOperator_domain {f : V → ℝ} (hf : ContDiff ℝ ∞ f)
    (hfc : HasCompactSupport f) :
    (memLp_of_contDiff_hasCompactSupport ν hf hfc).toLp f ∈
      (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain :=
  (LinearPMap.le_closure _).1
    (toLp_mem_domain_operator ν (ContinuousLinearMap.id ℝ V) _
      (IsTest.of_contDiff_hasCompactSupport ν _ hf hfc))
/-- The closed unit-weight gradient sends the class of a smooth compactly supported function to
the class of its gradient. -/
theorem closedWeightedOperator_toLp_eq {f : V → ℝ} (hf : ContDiff ℝ ∞ f)
    (hfc : HasCompactSupport f) :
    hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
        ⟨_, hν.toLp_mem_closedWeightedOperator_domain m hi hf hfc⟩ =
      (memLp_gradient_of_contDiff_hasCompactSupport hf hfc).toLp (gradient f) := by
  have htest := IsTest.of_contDiff_hasCompactSupport ν (ContinuousLinearMap.id ℝ V) hf hfc
  have hmem := toLp_mem_domain_operator ν (ContinuousLinearMap.id ℝ V)
    (hν.absolutelyContinuous_haar m hi) htest
  rw [← (LinearPMap.le_closure (hν.weightedOperator m (ContinuousLinearMap.id ℝ V) hi)).2
    (x := ⟨_, hmem⟩) (y := ⟨_, hν.toLp_mem_closedWeightedOperator_domain m hi hf hfc⟩) rfl,
    operator_apply ν (ContinuousLinearMap.id ℝ V) _ (hν.frontier_support_eq_zero hi) htest hmem rfl]
  exact MemLp.toLp_congr _ _ (Filter.Eventually.of_forall fun y => by rw [apply_id])
include hνU hU in
/-- **The weak identity on the domain of `T̄`**: for `f ∈ C_c^∞(V)` and every `x ∈ D(T̄)`,
`⟪[-ℒf], x⟫ = ⟪[∇f], T̄ x⟫` in `L²(ν)`. On smooth compactly supported classes this is weighted integration by parts; it
extends to `D(T̄)` because those classes are a graph-norm core of `T̄`. -/
theorem inner_toLp_neg_weightedLaplacian_eq {f : V → ℝ} (hf : ContDiff ℝ ∞ f)
    (hfc : HasCompactSupport f)
    (x : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain) :
    ⟪(memLp_neg_weightedLaplacian (ν := ν) hU hf hfc).toLp (fun y => -weightedLaplacian U f y),
        (x : Lp ℝ 2 (ν : Measure V))⟫ =
      ⟪(memLp_gradient_of_contDiff_hasCompactSupport hf hfc).toLp (gradient f),
        hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi x⟫ := by
  have hSclos : ((hν.weightedOperator m (ContinuousLinearMap.id ℝ V) hi).domRestrict
      (smoothCore ν)).closure = hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi :=
    hν.closure_domRestrict_eq_of_smoothCore_le m (ContinuousLinearMap.id ℝ V) hi le_rfl
      (smoothCore_le_domain_operator ν (ContinuousLinearMap.id ℝ V) _)
  have hSc : ((hν.weightedOperator m (ContinuousLinearMap.id ℝ V) hi).domRestrict
      (smoothCore ν)).IsClosable :=
    (hν.weightedOperator_isClosable m (ContinuousLinearMap.id ℝ V) hi).leIsClosable
      LinearPMap.domRestrict_le
  have hcore : ∀ y : ((hν.weightedOperator m (ContinuousLinearMap.id ℝ V) hi).domRestrict
      (smoothCore ν)).domain,
      ⟪(memLp_neg_weightedLaplacian (ν := ν) hU hf hfc).toLp (fun y => -weightedLaplacian U f y),
        (y : Lp ℝ 2 (ν : Measure V))⟫ =
      ⟪(memLp_gradient_of_contDiff_hasCompactSupport hf hfc).toLp (gradient f),
        (hν.weightedOperator m (ContinuousLinearMap.id ℝ V) hi).domRestrict (smoothCore ν) y⟫ := by
    rintro ⟨y, hy⟩
    have hy1 : y ∈ smoothCore ν := (Submodule.mem_inf.mp hy).1
    have hy2 : y ∈ (hν.weightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain :=
      (Submodule.mem_inf.mp hy).2
    obtain ⟨g, hg, hgc, rfl⟩ := hy1
    have htest := IsTest.of_contDiff_hasCompactSupport ν (ContinuousLinearMap.id ℝ V) hg hgc
    have hSy : (hν.weightedOperator m (ContinuousLinearMap.id ℝ V) hi).domRestrict (smoothCore ν)
        ⟨_, hy⟩ = htest.memLp_apply.toLp (apply (ContinuousLinearMap.id ℝ V) g) := by
      erw [LinearPMap.domRestrict_apply (x := ⟨_, hy⟩) (y := ⟨_, hy2⟩) rfl]
      exact operator_apply ν (ContinuousLinearMap.id ℝ V) _ (hν.frontier_support_eq_zero hi) htest
        hy2 rfl
    rw [hSy, L2.inner_def, L2.inner_def]
    have h1 : (fun a => ⟪((memLp_neg_weightedLaplacian (ν := ν) hU hf hfc).toLp
          (fun y => -weightedLaplacian U f y) : Lp ℝ 2 (ν : Measure V)) a,
          ((memLp_of_contDiff_hasCompactSupport ν hg hgc).toLp g : Lp ℝ 2 (ν : Measure V)) a⟫)
        =ᵐ[(ν : Measure V)] fun a => -weightedLaplacian U f a * g a := by
      filter_upwards [(memLp_neg_weightedLaplacian (ν := ν) hU hf hfc).coeFn_toLp,
        (memLp_of_contDiff_hasCompactSupport ν hg hgc).coeFn_toLp] with a ha hb
      rw [ha, hb, Real.inner_apply]
    have h2 : (fun a => ⟪((memLp_gradient_of_contDiff_hasCompactSupport hf hfc).toLp (gradient f) :
          Lp V 2 (ν : Measure V)) a,
          (htest.memLp_apply.toLp (apply (ContinuousLinearMap.id ℝ V) g) :
            Lp V 2 (ν : Measure V)) a⟫)
        =ᵐ[(ν : Measure V)] fun a => ⟪gradient f a, gradient g a⟫ := by
      filter_upwards [(memLp_gradient_of_contDiff_hasCompactSupport hf hfc).coeFn_toLp,
        htest.memLp_apply.coeFn_toLp] with a ha hb
      rw [ha, hb, apply_id]
    rw [integral_congr_ae h1, integral_congr_ae h2]
    exact (integral_inner_gradient_eq m hνU hU (hf.of_le (WithTop.coe_le_coe.mpr le_top)) hfc
      (hg.of_le (WithTop.coe_le_coe.mpr le_top))).symm
  have := inner_eq_inner_closure_apply hSc hcore
  rw [hSclos] at this
  exact this x
include hνU hU in
/-- **the smooth-test generator identity, domain clause**: for `f ∈ C_c^∞(V)`, the class `[f]` lies in `D(T̄†T̄)`. -/
theorem toLp_mem_adjointComp_domain {f : V → ℝ} (hf : ContDiff ℝ ∞ f)
    (hfc : HasCompactSupport f) :
    (memLp_of_contDiff_hasCompactSupport ν hf hfc).toLp f ∈
      (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain := by
  have hD := hν.toLp_mem_closedWeightedOperator_domain m hi hf hfc
  refine ⟨mem_adjointCompDomain.mpr ⟨hD, ?_⟩, hD⟩
  rw [hν.closedWeightedOperator_toLp_eq m hi hf hfc]
  exact LinearPMap.mem_adjoint_domain_of_exists _
    ⟨_, fun x => hν.inner_toLp_neg_weightedLaplacian_eq m hi hνU hU hf hfc x⟩
end Generator
end LogConcave
end KLS
end FunctionalInequalities

Source

Source: Klartag–Lehec, Bourgain’s slicing problem and KLS isoperimetry up to polylog (arXiv:2203.15551v2), item E14. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HeatSemigroup/Generator.lean#L59-L198 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Generator`, definition bundle `KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Generator`; the repository is private at upload time).

View graph