Generator: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

The negative-generator integral pairing
The squared-centering integral called variance
The three finite-integral obligations for Poincaré's inequality
The generator Poincaré predicate
The totalized density-entropy integral
The five density-domain conditions for log-Sobolev
The generator log-Sobolev predicate with factor C/2

Samplinglib mathematical lesson

The negative-generator integral pairing

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

Read this first

Mathematical statement

For a measure μ on a measurable space E, an arbitrary operator L on real-valued functions, and observables f,g:E→ℝ, define the generator Dirichlet pairing to be minus the μ-integral of f times Lg. No symmetry, positivity or operator linearity is part of this definition.

\[\mathcal E_\mu^L(f,g):=-\int_E f(x)(Lg)(x)\,d\mu(x).\]

Lean statement · dirichletForm

The operator parameter is a function taking functions to functions; it is not a linear-map parameter. The return value is a real number, not a bilinear-form structure with proved laws.

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)

noncomputable def dirichletForm
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (f g : E → ℝ) : ℝ

Exact module and namespace context

Proof roadmap

1Apply the operator to the second argument
First form the function Lg and multiply its value by the first observable f.
2Negate its integral
The definition fixes the negative-generator sign convention. With integrability, this is the usual finite pairing; without it the real integral remains totalized.

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,g:E→ℝ are arbitrary; no integrability premise.

Construction and meaning

1. Apply the operator to the second argument

First form the function Lg and multiply its value by the first observable f.

\[u(x):=f(x)(Lg)(x).\]

Corresponding Lean step

generator g; pointwise real multiplication

2. Negate its integral

The definition fixes the negative-generator sign convention. With integrability, this is the usual finite pairing; without it the real integral remains totalized.

\[\mathcal E_\mu^L(f,g)=-\int_Eu\,d\mu.\]

Corresponding Lean step

MeasureTheory.integral; Generator.dirichletForm

Lean verification

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

Lean construction · dirichletForm

This is a construction only: apply L to g, multiply by f, integrate, and negate. No integration-by-parts, symmetry or nonnegativity proof occurs.

Download module (.lean)

noncomputable def dirichletForm
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (f g : E → ℝ) : ℝ :=
  -(∫ x, f x * generator g x ∂mu)

Exact module and namespace context

Scope and omitted-condition boundaries

All integrals are real Bochner integrals. An integral is totalized to zero when its integrand is not integrable; writing the integral does not prove a genuine finite expectation or energy.
No global invariant-law, stationarity for every observable, reversibility, semigroup construction, or concrete diffusion identity is inferred from this declaration.
Calling this a Dirichlet form does not assert bilinearity, closedness, positivity, or a Hilbert-space form domain.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.integral

Mathematical sources

Exact existing ASTIS declaration — Current statement and body; renderer extracts exact Lean rather than duplicating it in this packet.
Totalized Bochner integral — integral_undef explains the nonintegrable case; it is background, not a call in this definition.
Existing focused test — Declaration-visibility #check only. No test/build run for this packet.

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

Samplinglib mathematical lesson

The squared-centering integral called variance

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

Read this first

Mathematical statement

For any measure μ on a measurable space E and any function f:E→ℝ, define m=∫f dμ and variance μ f=∫(f−m)² dμ. The definition does not normalize μ. It represents the usual probability variance only when the relevant probability and integrability conditions are supplied.

\[m_\mu(f):=\int_E f\,d\mu,\qquad\operatorname{Var}_\mu(f):=\int_E\big(f(x)-m_\mu(f)\big)^2\,d\mu(x).\]

Lean statement · variance

The declaration accepts an arbitrary measure. Its displayed center has no mass-normalization factor, so probability-language interpretation must not be applied automatically.

Download module (.lean)

noncomputable def variance (mu : Measure E) (f : E → ℝ) : ℝ

Exact module and namespace context

Proof roadmap

1Choose the displayed center
The center is the integral itself, not that integral divided by μ(E). It is a real-valued expression under the totalized convention.
2Integrate the squared displacement from that center
Subtract the same scalar m at every point, square, and integrate under μ.

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.
f:E→ℝ is arbitrary. No probability, finite-total-mass, integrability, or square-integrability premise; no operator is an input.

Construction and meaning

1. Choose the displayed center

The center is the integral itself, not that integral divided by μ(E). It is a real-valued expression under the totalized convention.

\[m:=\int_Ef\,d\mu.\]

Corresponding Lean step

MeasureTheory.integral

2. Integrate the squared displacement from that center

Subtract the same scalar m at every point, square, and integrate under μ.

\[\operatorname{Var}_\mu(f)=\int_E(f-m)^2\,d\mu.\]

Corresponding Lean step

Generator.variance

Lean verification

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

Lean construction · variance

There is no theorem proof: form the inner integral, then form and integrate the centered square. Both integrals are totalized unless their integrability is known.

Download module (.lean)

noncomputable def variance (mu : Measure E) (f : E → ℝ) : ℝ :=
  ∫ x, (f x - ∫ y, f y ∂mu) ^ 2 ∂mu

Exact module and namespace context

Scope and omitted-condition boundaries

All integrals are real Bochner integrals. An integral is totalized to zero when its integrand is not integrable; writing the integral does not prove a genuine finite expectation or energy.
For general μ this is not automatically the variance of the normalized law μ/μ(E). No normalization or finite-variance theorem is asserted.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.integral

Mathematical sources

Exact existing ASTIS declaration — Current statement and body; renderer extracts exact Lean rather than duplicating it in this packet.

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

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.

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.

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.

Download module (.lean)

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

Exact module and namespace context

Proof roadmap

1Require a probability measure and positive constant
These are the first two parts of a certificate for this predicate.
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.

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

Exact existing ASTIS declaration — Current statement and body; renderer extracts exact Lean rather than duplicating it in this packet.
Existing source-correspondence record: chewi-1-2-definition-1-2-19 — Existing local record for Chewi Definition1.2.19, edition2026-08-09, printed p.16/PDF p.28. Reported only within the current declaration's explicit assumptions; no new source audit or source-equivalence verdict.
Probability-measure class — The class means μ(univ)=1; no extra state-space topology is introduced.
Existing focused test — Declaration-visibility #check only. No test/build run for this packet.

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

Samplinglib mathematical lesson

The totalized density-entropy integral

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

Read this first

Mathematical statement

For any measure μ on a measurable space E and any real-valued function ρ, define densityEntropy μ ρ=∫ρ logρ dμ using Mathlib's totalized real logarithm. No nonnegative-density, normalization, probability, or integrability condition is included in this definition.

\[H_\mu(\rho):=\int_E\rho(x)\operatorname{Real.log}(\rho(x))\,d\mu(x),\qquad0\cdot\operatorname{Real.log}(0)=0.\]

Lean statement · densityEntropy

The name suggests a density interpretation, but the signature accepts arbitrary real functions and arbitrary measures. The later admissibility predicate supplies the conditions needed for that interpretation.

Download module (.lean)

noncomputable def densityEntropy (mu : Measure E) (rho : E → ℝ) : ℝ

Exact module and namespace context

Proof roadmap

1Form the entropy integrand
Multiply each value of ρ by its totalized real logarithm. At zero the product is zero. Values of ρ are not restricted by this definition.
2Integrate against the explicit base
Take the real Bochner integral of u, with its standard totalization outside the integrable domain.

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.
ρ:E→ℝ is arbitrary; it is not supplied as a selected RN representative, nor assumed nonnegative or normalized.
No operator is an input and no integrability hypothesis is required to form the expression.

Construction and meaning

1. Form the entropy integrand

Multiply each value of ρ by its totalized real logarithm. At zero the product is zero. Values of ρ are not restricted by this definition.

\[u(x):=\rho(x)\operatorname{Real.log}(\rho(x)).\]

Corresponding Lean step

Real.log

2. Integrate against the explicit base

Take the real Bochner integral of u, with its standard totalization outside the integrable domain.

\[H_\mu(\rho)=\int_Eu\,d\mu.\]

Corresponding Lean step

MeasureTheory.integral; Generator.densityEntropy

Lean verification

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

Lean construction · densityEntropy

This is a construction, not a KL theorem. It forms the product with the real logarithm and integrates it; it neither constructs a density measure nor identifies this expression with canonical KL.

Download module (.lean)

noncomputable def densityEntropy (mu : Measure E) (rho : E → ℝ) : ℝ :=
  ∫ x, rho x * Real.log (rho x) ∂mu

Exact module and namespace context

Scope and omitted-condition boundaries

All integrals are real Bochner integrals. An integral is totalized to zero when its integrand is not integrable; writing the integral does not prove a genuine finite expectation or energy.
No equality with InformationTheory.klDiv, no nonnegativity, and no genuine relative-entropy interpretation is established for arbitrary signed or unnormalized ρ.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Real.log
MeasureTheory.integral

Mathematical sources

Exact existing ASTIS declaration — Current statement and body; renderer extracts exact Lean rather than duplicating it in this packet.
Totalized real logarithm and its zero value — Real.log is defined on all reals; log_zero is at103.

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

Samplinglib mathematical lesson

The five density-domain conditions for log-Sobolev

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

Read this first

Mathematical statement

For a measure μ on a measurable space E, an arbitrary operator L on real functions, and ρ:E→ℝ, LogSobolevAdmissible means: ρ is pointwise nonnegative; ρ is μ-integrable; ∫ρ dμ=1; ρ logρ is μ-integrable; and ρ L(logρ) is μ-integrable. Here logρ is the exact totalized function x↦Real.log(ρ(x)).

\[\begin{aligned}\mathcal A_{LS}(\mu,L,\rho)\ :\Longleftrightarrow\;&(\forall x,\ 0\le\rho(x))\ \land\ \rho\in L^1(\mu)\ \land\ \int_E\rho\,d\mu=1\\&\land\ \rho\log\rho\in L^1(\mu)\ \land\ \rho L(\log\rho)\in L^1(\mu).\end{aligned}\]

Lean statement · LogSobolevAdmissible

This is a five-part logical proposition, not a structure with generated named fields. It supplies no differentiability or chain rule for the logarithm at zero-density points.

Download module (.lean)

def LogSobolevAdmissible
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (rho : E → ℝ) : Prop

Exact module and namespace context

Proof roadmap

1Require a nonnegative integrable normalized weight
Supply the sign, integrability, and unit-integral statements separately.
2Require finite entropy integrability
Demand integrability of the product with the totalized logarithm; integrability of ρ alone does not supply it.
3Require finite generator pairing and collect the domain
Demand integrability of ρ times L applied to the full log function. This last condition controls the Dirichlet pairing used in the inequality.

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.
ρ is arbitrary when the predicate is formed. All five listed properties must be proved to construct a witness.
Integrable means a.e. strong measurability together with finite integral of the norm, not merely existence of the totalized integral expression.
Nonnegativity is pointwise, not merely μ-a.e. The base measure is not required to be probability by this predicate itself.

Construction and meaning

1. Require a nonnegative integrable normalized weight

Supply the sign, integrability, and unit-integral statements separately.

\[\rho\ge0,\qquad\rho\in L^1(\mu),\qquad\int_E\rho\,d\mu=1.\]

Corresponding Lean step

Generator.LogSobolevAdmissible: first three conjuncts

2. Require finite entropy integrability

Demand integrability of the product with the totalized logarithm; integrability of ρ alone does not supply it.

\[\rho\operatorname{Real.log}\rho\in L^1(\mu).\]

Corresponding Lean step

MeasureTheory.Integrable

3. Require finite generator pairing and collect the domain

Demand integrability of ρ times L applied to the full log function. This last condition controls the Dirichlet pairing used in the inequality.

\[\rho L(\operatorname{Real.log}\rho)\in L^1(\mu).\]

Corresponding Lean step

Generator.LogSobolevAdmissible: last conjunct

Lean verification

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

Lean construction · LogSobolevAdmissible

Construct a witness by proving every listed condition. In particular, neither entropy integrability nor generator-pairing integrability is inferred from normalization.

Download module (.lean)

def LogSobolevAdmissible
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (rho : E → ℝ) : Prop :=
  (0 ≤ rho) ∧
    Integrable rho mu ∧
    (∫ x, rho x ∂mu) = 1 ∧
    Integrable (fun x => rho x * Real.log (rho x)) mu ∧
    Integrable (fun x => rho x * generator (fun y => Real.log (rho y)) 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 strict positivity, smoothness, RN representative choice, generator-domain stability, or closed Dirichlet-form/Sobolev domain is imposed.
The operator is arbitrary on pointwise functions; the predicate does not grant invariance under changing ρ on a null set.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Integrable
MeasureTheory.integral
Real.log

Mathematical sources

Exact existing ASTIS declaration — Current statement and body; renderer extracts exact Lean rather than duplicating it in this packet.
Integrability includes measurability and finite norm integral — Exact domain meaning.

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

Samplinglib mathematical lesson

The generator log-Sobolev predicate with factor C/2

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

Read this first

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

\[\begin{aligned}\operatorname{LSI}(\mu,L,C)\ :\Longleftrightarrow\;&\mu(E)=1\ \land\ C>0\\&\land\ \forall\rho:E\to\mathbb R,\ \mathcal A_{LS}(\mu,L,\rho)\Rightarrow H_\mu(\rho)\le\frac C2\mathcal E_\mu^L(\rho,\log\rho).\end{aligned}\]

Lean statement · SatisfiesLogSobolev

The universal estimate is part of what this proposition means. The return type is a proposition, not a theorem producing log-Sobolev from curvature or reversibility.

Download module (.lean)

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

Exact module and namespace context

Proof roadmap

1Require normalization and a positive constant
These two conjuncts establish the law and constant used by the inequality.
2Demand the normalized density inequality
For every admissible density, compare the defined entropy integral with the negative-generator pairing and retain the exact factor one-half.

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

1. Require normalization and a positive constant

These two conjuncts establish the law and constant used by the inequality.

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

Corresponding Lean step

MeasureTheory.IsProbabilityMeasure; Generator.SatisfiesLogSobolev

2. Demand the normalized density inequality

For every admissible density, compare the defined entropy integral with the negative-generator pairing and retain the exact factor one-half.

\[\int_E\rho\log\rho\,d\mu\le-\frac C2\int_E\rho L(\log\rho)\,d\mu.\]

Corresponding Lean step

Generator.LogSobolevAdmissible; Generator.densityEntropy; Generator.dirichletForm

Lean verification

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

Lean construction · SatisfiesLogSobolev

This definition packages normalization, positivity of C, and the displayed inequality on its explicit domain. It does not prove any particular model satisfies it or equate its Dirichlet pairing with canonical Fisher information.

Download module (.lean)

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

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 Bakry–Émery-to-LSI theorem, KL/entropy identification, density-flow dissipation, canonical Fisher bridge, or convergence rate is proved by this definition.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.IsProbabilityMeasure

Mathematical sources

Exact existing ASTIS declaration — Current statement and body; renderer extracts exact Lean rather than duplicating it in this packet.
Existing source-correspondence record: chewi-1-2-definition-1-2-25 — Existing local record for Chewi Definition1.2.25, edition2026-08-09, printed p.18/PDF p.30. Reported only within the current declaration's explicit assumptions; no new source audit or source-equivalence verdict.
Existing focused test — Declaration-visibility #check only. No test/build run for this packet.

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