Prove2Me

Constant function in the heat-semigroup form domain

Definition
KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Markov

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a full-dimensional log-concave probability measure ν\nu and any bounded linear weight BB, one_mem_domain_closedWeightedOperator states that the constant class L2.const ν 1 belongs to the domain of closedWeightedOperator, provided (int⁡supp⁡ν)≠∅(\operatorname{int}\operatorname{supp}\nu)\ne\varnothing. This is an auxiliary domain statement for the closed weighted-gradient operator; it does not itself state the Markov properties of the semigroup.

Original module imports

import FunctionalInequalities.Analysis.Semigroup.Generated.Markov
import FunctionalInequalities.Energy.SmoothGradient.Dirichlet
import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Basic

Original declaration excerpt

Shown in the original module context.

theorem one_mem_domain_closedWeightedOperator (hν : LogConcave ν)
    (hi : (interior (ν : Measure V).support).Nonempty) :
    L2.const ν 1 ∈ (hν.closedWeightedOperator m B hi).domain := by
  let hac := hν.absolutelyContinuous_haar m hi
  rw [WeightedGradient.L2_const_eq_toLp]
  exact (hν.weightedOperator m B hi).le_closure.1
    (WeightedGradient.toLp_mem_domain_operator ν B hac (WeightedGradient.IsTest.const 1))

Module navigation

Direct project imports: Analysis/Semigroup/Generated/Markov, Energy/SmoothGradient/Dirichlet, KLS/LogConcave/HeatSemigroup/Basic.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Semigroup_Generated_Markov
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_SmoothGradient_Dirichlet
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Basic

noncomputable section
open Filter InnerProductSpace MeasureTheory Topology
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
open Energy Energy.Euclidean
open FunctionalInequalities.Analysis.Semigroup
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : ProbabilityMeasure V} (m : Measure V) [m.IsAddHaarMeasure] (B : V →L[ℝ] V)
/-- The constant one belongs to the domain of the closed weighted gradient. -/
theorem one_mem_domain_closedWeightedOperator (hν : LogConcave ν)
    (hi : (interior (ν : Measure V).support).Nonempty) :
    L2.const ν 1 ∈ (hν.closedWeightedOperator m B hi).domain := by
  let hac := hν.absolutelyContinuous_haar m hi
  rw [WeightedGradient.L2_const_eq_toLp]
  exact (hν.weightedOperator m B hi).le_closure.1
    (WeightedGradient.toLp_mem_domain_operator ν B hac (WeightedGradient.IsTest.const 1))
end LogConcave
end KLS
end FunctionalInequalities
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HeatSemigroup/Markov.lean#L223-L230 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Markov`, definition bundle `KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Markov`; the repository is private at upload time).

View graph