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

ASTIS mathematical exposition

The negative-generator integral pairing

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

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).\]

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

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

Exact module and namespace context

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.

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

/-- Variance as the squared centered `L2(mu)` norm. -/

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.

Source and reuse

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

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

ASTIS mathematical exposition

The squared-centering integral called variance

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

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).\]

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

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

Exact module and namespace context

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.

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

/-- Domain conditions needed to read both sides of the generator Poincare
inequality as genuine finite integrals. -/

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.

Source and reuse

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

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

ASTIS mathematical exposition

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

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

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).\]

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 statement · PoincareAdmissible

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

def PoincareAdmissible
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (f : E → ℝ) : Prop

Exact module and namespace context

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.

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

/-- Chewi Definition 1.2.19: the generator Poincare inequality
`Var_mu(f) <= C * E(f,f)` for every admissible observable. -/

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.

Source and reuse

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

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

ASTIS mathematical exposition

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.

\[\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}\]

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

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

Exact module and namespace context

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.

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`. -/

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.

Source and reuse

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

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

ASTIS mathematical exposition

The totalized density-entropy integral

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

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.\]

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

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

Exact module and namespace context

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.

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

/-- Domain conditions for the density formulation of log-Sobolev. -/

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

Source and reuse

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

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

ASTIS mathematical exposition

The five density-domain conditions for log-Sobolev

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

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}\]

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

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

Exact module and namespace context

Lean construction · LogSobolevAdmissible

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

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

/-- Chewi Definition 1.2.25: the density log-Sobolev inequality
`KL(rho mu || mu) <= (C/2) E(rho, log rho)`. -/

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.

Source and reuse

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

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

ASTIS mathematical exposition

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

\[\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}\]

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

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

Exact module and namespace context

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.

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.

Source and reuse

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

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