Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

The generator Poincaré predicate

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

Read this first

Mathematical 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.

\[\begin{aligned}\operatorname{Poincare}(\mu,L,C)\ :\Longleftrightarrow\;&\mu(E)=1\ \land\ C>0\\&\land\ \forall f:E\to\mathbb R,\ \mathcal A_P(\mu,L,f)\Rightarrow\operatorname{Var}_\mu(f)\le C\mathcal E_\mu^L(f,f).\end{aligned}\]
Lean statement · SatisfiesPoincare

The probability condition is stored inside the proposition rather than assumed in brackets. The declaration does not require L to be a linear or Markov operator.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
def SatisfiesPoincare
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (C : ℝ) : Prop

Exact module and namespace context

Proof roadmap

  1. 1Require a probability measure and positive constant

    These are the first two parts of a certificate for this predicate.

  2. 2Require the inequality on the explicit domain

    For every f, a proof of the three admissibility conditions must yield the variance-versus-energy estimate.

Full assumptions and notation

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

1. Require a probability measure and positive constant

These are the first two parts of a certificate for this predicate.

\[\mu(E)=1,\qquad C>0.\]
Corresponding Lean step

MeasureTheory.IsProbabilityMeasure; Generator.SatisfiesPoincare

2. Require the inequality on the explicit domain

For every f, a proof of the three admissibility conditions must yield the variance-versus-energy estimate.

\[\mathcal A_P(\mu,L,f)\Longrightarrow\int_E(f-\textstyle\int_E f\,d\mu)^2d\mu\le-C\int_EfLf\,d\mu.\]
Corresponding Lean step

Generator.PoincareAdmissible; Generator.variance; Generator.dirichletForm

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean construction · SatisfiesPoincare

This is a definition of what a Poincaré certificate must establish: normalization, positive C, and an estimate for every admissible observable. It does not produce such a certificate or prove decay.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
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

Exact module and namespace context

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.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • MeasureTheory.IsProbabilityMeasure

Mathematical sources

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.