Samplinglib mathematical lesson

The real Radon–Nikodym density also has unit integral

AutoSamplingTheory.lsiKlFiRnDerivDensityMassOne · theorem · Teaching coverage

Read this first

Mathematical statement

For absolutely continuous probability measures ρ≪π, the real-valued function r=(dρ/dπ).toReal has real integral one against π.

\[\int_\alpha r(x)\,d\pi(x)=1,\qquad r=(d\rho/d\pi)_{\mathrm{toReal}}.\]

Lean statement · lsiKlFiRnDerivDensityMassOne

The integrand is a particular real conversion of the extended Radon–Nikodym derivative, not an unspecified density symbol.

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

Exact module and namespace context

Proof roadmap

1Apply real Radon–Nikodym mass transport
The imported theorem expresses the integral of the real conversion as the real total mass of ρ. Sigma-finiteness is available from the probability instances.
2Simplify the total mass
The real conversion of probability mass one 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. Apply real Radon–Nikodym mass transport

The imported theorem expresses the integral of the real conversion as the real total mass of ρ. Sigma-finiteness is available from the probability instances.

\[\int R_{\mathrm{toReal}}\,d\pi=\rho.\mathrm{real}(\alpha).\]

Corresponding Lean step

Measure.integral_toReal_rnDeriv hrho_pi

2. Simplify the total mass

The real conversion of probability mass one is one.

\[\rho.\mathrm{real}(\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 · lsiKlFiRnDerivDensityMassOne

The proof reuses the real mass theorem and simplifies probability mass; it does not establish a smooth density.

Download module (.lean)

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

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Measure.integral_toReal_rnDeriv

Mathematical sources

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