The generator log-Sobolev predicate with factor C/2

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.SatisfiesLogSobolev · def · Teaching coverage

Statement

Given a measure μ on a measurable space E, an arbitrary operator L on real functions, and C∈ℝ, SatisfiesLogSobolev means that μ is probability, C>0, and every LogSobolev-admissible ρ satisfies Hμ(ρ)≤(C/2)Eμ^L(ρ,logρ). Admissibility includes pointwise nonnegativity, integrability and unit integral of ρ, plus integrability of ρ logρ and ρ L(logρ).

All objects and hypotheses

• E is any measurable space and μ is any measure on E, unless probability normalization is explicitly included below. No topology, norm, finite dimension, σ-finiteness, or nonempty-space premise is imposed.
• L:(E→ℝ)→(E→ℝ) is an arbitrary operator on real functions. This signature does not require linearity, measurability preservation, Markovness, or a semigroup.
• C is a real input. Probability normalization and positivity of C are assertions inside this predicate, not prerequisites for forming it.
• The quantifier ranges over all real functions, with the inequality conditional on all five LogSobolevAdmissible requirements.

Construction and meaning

def SatisfiesLogSobolev
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (C : ℝ) : Prop

def SatisfiesLogSobolev
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (C : ℝ) : Prop :=
  IsProbabilityMeasure mu ∧ 0 < C ∧
    ∀ rho : E → ℝ, LogSobolevAdmissible mu generator rho →
      densityEntropy mu rho ≤
        (C / 2) * dirichletForm mu generator rho (fun x => Real.log (rho x))

end Generator
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

Scope and omitted-condition boundaries

• This defines a proposition that must be proved for a concrete model. It does not prove existence of a witness or derive an inequality from the operator's name.
• No global invariant-law, stationarity for every observable, reversibility, semigroup construction, or concrete diffusion identity is inferred from this declaration.
• No Bakry–Émery-to-LSI theorem, KL/entropy identification, density-flow dissipation, canonical Fisher bridge, or convergence rate is proved by this definition.