Samplinglib mathematical lesson

The Radon–Nikodym density has unit nonnegative integral

AutoSamplingTheory.lsiKlFiRnDerivLIntegralMassOne · theorem · Teaching coverage

Read this first

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

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.

Download module (.lean)

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

Proof roadmap

1Recover the mass from the derivative
The Radon–Nikodym mass identity under absolute continuity identifies the lower integral with the total mass of ρ.
2Use probability normalization
The total mass of ρ is one.

Full assumptions and notation

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 verification

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

Lean proof · lsiKlFiRnDerivLIntegralMassOne

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

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

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

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