ASTIS mathematical exposition

The Radon–Nikodym density has unit nonnegative integral

AutoSamplingTheory.lsiKlFiRnDerivLIntegralMassOne · theorem · Teaching coverage

Statement

For probability measures ρ and π on a measurable space with ρ≪π, the nonnegative extended integral of dρ/dπ against π equals one.

\[\int_\alpha^{\!-}\frac{d\rho}{d\pi}\,d\pi=\rho(\alpha)=1.\]

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. Recover the mass from the derivative

The Radon–Nikodym mass identity under absolute continuity identifies the lower integral with the total mass of ρ.

\[\int^{\!-}R\,d\pi=\rho(\alpha).\]

Corresponding Lean step

Measure.lintegral_rnDeriv hrho_pi

2. Use probability normalization

The total mass of ρ is one.

\[\rho(\alpha)=1.\]

Corresponding Lean step

simp

Lean statement · lsiKlFiRnDerivLIntegralMassOne

This is the extended nonnegative integral, not the real Bochner integral; its integrand can take extended values.

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 lsiKlFiRnDerivLIntegralMassOne {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫⁻ x, rho.rnDeriv pi x ∂pi = 1

Exact module and namespace context

Lean proof · lsiKlFiRnDerivLIntegralMassOne

The first rewrite uses the existing Radon–Nikodym theorem. Probability normalization simplifies the remaining total mass.

theorem lsiKlFiRnDerivLIntegralMassOne {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫⁻ x, rho.rnDeriv pi x ∂pi = 1 := by
  rw [Measure.lintegral_rnDeriv hrho_pi]
  simp

/-- Real-integral normalization of the Radon-Nikodym density ratio.

This supplies the real mass input used by the scalar normalization bridge for
the LSI test `phi=sqrt(d rho/d pi)`.
-/

Exact module and namespace context

Scope and omitted-condition boundaries

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.
No differentiability or admissible square-root test follows from unit mass.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.Measure.lintegral_rnDeriv
MeasureTheory.IsProbabilityMeasure.measure_univ

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
MeasureTheory.Measure.lintegral_rnDeriv — 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.