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.

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.

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.