Samplinglib mathematical lesson

The three finite-integral obligations for Poincaré's inequality

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

Read this first

Mathematical statement

For a measure μ on a measurable space E, an arbitrary operator L, and f:E→ℝ, PoincareAdmissible means exactly that f, its squared displacement from ∫f dμ, and the generator pairing integrand fLf are μ-integrable. The predicate itself neither assumes μ is probability nor imposes linearity on L.

\[\mathcal A_P(\mu,L,f)\ :\Longleftrightarrow\ f\in L^1(\mu)\ \land\ (f-\textstyle\int_E f\,d\mu)^2\in L^1(\mu)\ \land\ fLf\in L^1(\mu).\]

Lean statement · PoincareAdmissible

This definition returns a proposition. Its conjunction components are real proof obligations, not metadata fields or automatically established regularity.

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 PoincareAdmissible
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (f : E → ℝ) : Prop

Exact module and namespace context

Proof roadmap

1Require an integrable observable
This gives a genuine finite centering integral.
2Require an integrable centered square
This is the precise variance integrand used by this module, not an unstated equivalent domain.
3Require an integrable generator pairing and collect the conditions
The last condition makes the quadratic Dirichlet pairing a finite integral. The three proofs are joined by logical conjunction.

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.
f:E→ℝ is arbitrary when the predicate is formed. To inhabit it, all three stated integrability facts must be proved.
Integrable means a.e. strong measurability together with finite integral of the norm, not merely existence of the totalized integral expression.

Construction and meaning

1. Require an integrable observable

This gives a genuine finite centering integral.

\[f\in L^1(\mu).\]

Corresponding Lean step

MeasureTheory.Integrable

2. Require an integrable centered square

This is the precise variance integrand used by this module, not an unstated equivalent domain.

\[(f-\textstyle\int_E f\,d\mu)^2\in L^1(\mu).\]

Corresponding Lean step

Generator.variance integrand

3. Require an integrable generator pairing and collect the conditions

The last condition makes the quadratic Dirichlet pairing a finite integral. The three proofs are joined by logical conjunction.

\[fLf\in L^1(\mu),\qquad\mathcal A_P\equiv A_1\land A_2\land A_3.\]

Corresponding Lean step

Generator.PoincareAdmissible; And

Lean verification

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

Lean construction · PoincareAdmissible

Constructing a witness requires supplying each of the three integrability proofs. No one component is derived from another, and no witness is created by the definition.

Download module (.lean)

def PoincareAdmissible
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (f : E → ℝ) : Prop :=
  Integrable f mu ∧
    Integrable (fun x => (f x - ∫ y, f y ∂mu) ^ 2) mu ∧
    Integrable (fun x => f x * generator f x) mu

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 probability normalization, operator-domain closure or global L² theorem is included.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Integrable
MeasureTheory.integral

Mathematical sources

Exact existing ASTIS declaration — Current statement and body; renderer extracts exact Lean rather than duplicating it in this packet.
Exact integrability predicate — Integrable includes a.e. strong measurability and finite integral of the norm.

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