The generator Poincaré predicate

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

Statement

Given a measure μ on a measurable space E, any operator L on real functions, and C∈ℝ, SatisfiesPoincare means that μ is a probability measure, C>0, and every Poincare-admissible f satisfies Varμ(f)≤C Eμ^L(f,f). Admissibility requires μ-integrability of f, its centered square, and fLf.

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 an arbitrary real input to the predicate; positivity and probability normalization are required conjuncts, not ambient typeclass assumptions.
• The universal quantifier is over all real functions; the inequality is required only when all three PoincareAdmissible integrability conditions hold.

Construction and meaning

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

def SatisfiesPoincare
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (C : ℝ) : Prop :=
  IsProbabilityMeasure mu ∧ 0 < C ∧
    ∀ f : E → ℝ, PoincareAdmissible mu generator f →
      variance mu f ≤ C * dirichletForm mu generator f f

/-- Relative entropy of a density `rho` with respect to its reference
probability measure.  Mathlib's totalized `Real.log 0 = 0` gives the standard
zero-density convention in the product `rho * log rho`. -/

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 spectral-gap equivalence, semigroup variance dissipation, or exponential-convergence theorem is supplied.