ASTIS mathematical exposition

Transport the density entropy integral to the log-likelihood measure

AutoSamplingTheory.lsiKlFiRnDerivEntropyIntegral · theorem · Teaching coverage

Statement

For probability measures ρ≪π, with r=(dρ/dπ).toReal and ℓρ,π=log r, the real integral ∫r log r dπ equals ∫ℓρ,π dρ. This is equality of Mathlib's totalized real integrals; it does not assert their integrability or finiteness as entropy quantities.

\[\int_\alpha r(x)\log r(x)\,d\pi(x)=\int_\alpha\ell_{\rho,\pi}(x)\,d\rho(x).\]

All objects and hypotheses

α is an arbitrary measurable space; ρ and π are measures on it, both with IsProbabilityMeasure instances.
hrho_pi supplies absolute continuity ρ≪π. Probability assumptions supply the finite/sigma-finite and Lebesgue-decomposition requirements of the imported Radon–Nikodym APIs.
Write R=dρ/dπ for Mathlib's ℝ≥0∞-valued rnDeriv representative and r=R.toReal for its real-valued conversion; r≥0 everywhere.

Notation and interpretation

Integrability and Bochner integrals: L¹ in the teaching formulas means Integrable, not a newly defined quotient-space element. ∫ denotes Mathlib's totalized Bochner integral: it is zero for nonintegrable functions, and also for a codomain lacking completeness. Do not infer integrability or a genuine finite expectation from an unqualified integral equality. Real-valued integrals have a complete codomain; missing integrability still matters.
\[f\in L^1(\mu)\quad\Longleftrightarrow\quad f\text{ is a.e. strongly measurable and }\int^{\!-}\|f\|\,d\mu<\infty\]

Mathematical proof

1. Use the log-likelihood Radon–Nikodym transport identity

The imported identity changes the reference measure from π weighted by its density r to ρ. Its sigma-finite/decomposition requirements are supplied by the probability assumptions.

\[\int r\log r\,d\pi=\int\log r\,d\rho.\]

Corresponding Lean step

integral_rnDeriv_mul_log hrho_pi

Lean statement · lsiKlFiRnDerivEntropyIntegral

No integrability assumption appears in this theorem. The right side is the real log-likelihood integral, not an assertion that extended KL is finite.

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.

theorem lsiKlFiRnDerivEntropyIntegral {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫ x, (rho.rnDeriv pi x).toReal * Real.log (rho.rnDeriv pi x).toReal ∂pi =
      ∫ x, llr rho pi x ∂rho

Exact module and namespace context

Lean proof · lsiKlFiRnDerivEntropyIntegral

This is direct reuse of the log-likelihood-ratio change-of-measure theorem. Its general integral convention allows the equality even when the analytic entropy integral is not finite.

theorem lsiKlFiRnDerivEntropyIntegral {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫ x, (rho.rnDeriv pi x).toReal * Real.log (rho.rnDeriv pi x).toReal ∂pi =
      ∫ x, llr rho pi x ∂rho := by
  exact integral_rnDeriv_mul_log hrho_pi

/-- Entropy transport for the square-root density test used by LSI.

This rewrites the LSI entropy integrand for
`phi=sqrt(d rho/d pi)` and then uses the Radon-Nikodym entropy transport
identity.  It still does not prove admissibility of `phi` or the Fisher
chain-rule side of `eq:LSI-KL-FI`.
-/

Exact module and namespace context

Scope and omitted-condition boundaries

∫ denotes Mathlib's totalized Bochner integral: it is zero for nonintegrable functions, and also for a codomain lacking completeness. Do not infer integrability or a genuine finite expectation from an unqualified integral equality. Real-valued integrals have a complete codomain; missing integrability still matters.
The chosen real density r is (rnDeriv ρ π).toReal, with ENNReal.toReal(∞)=0. Do not replace this with an arbitrary pointwise density version; absolute continuity and probability measures justify the a.e. density interpretation.
These are scalar, density-integral or supplied-derivative handoffs. They do not prove an LSI, the admissibility of its square-root-density test, the vector/Sobolev chain rule or the full KL–Fisher comparison.
Do not identify this equality alone with a finite KL formula; downstream hypotheses must control the log-likelihood integral.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.integral_rnDeriv_mul_log
MeasureTheory.llr

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
MeasureTheory.integral_rnDeriv_mul_log — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
MeasureTheory.llr — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.

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