Samplinglib mathematical lesson

The squared square-root Radon–Nikodym test has unit mass

AutoSamplingTheory.lsiKlFiSqrtRnDerivTestMassOne · theorem · Teaching coverage

Read this first

Mathematical statement

For probability measures ρ≪π and r=(dρ/dπ).toReal, the real integral of (√r)² against π is one.

\[\int_\alpha(\sqrt{r(x)})^2\,d\pi(x)=1.\]

Lean statement · lsiKlFiSqrtRnDerivTestMassOne

The measure assumptions give density mass. Nonnegativity of the real conversion supplies the pointwise square identity.

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

Exact module and namespace context

Proof roadmap

1Replace the target one by the density's known mass
The preceding real-density theorem gives ∫r dπ=1, reducing the claim to equality of two integrals.
2Compare the integrands pointwise
The real conversion r is nonnegative everywhere, so its square root squares to r at every x, and therefore π-a.e.
3Transfer a.e. equality through integration
A.e.-equal integrands have equal totalized real integrals.

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. Replace the target one by the density's known mass

The preceding real-density theorem gives ∫r dπ=1, reducing the claim to equality of two integrals.

\[1=\int r\,d\pi.\]

Corresponding Lean step

rw [← lsiKlFiRnDerivDensityMassOne rho pi hrho_pi]

2. Compare the integrands pointwise

The real conversion r is nonnegative everywhere, so its square root squares to r at every x, and therefore π-a.e.

\[(\sqrt{r(x)})^2=r(x)\quad\forall x.\]

Corresponding Lean step

Real.sq_sqrt ENNReal.toReal_nonneg

3. Transfer a.e. equality through integration

A.e.-equal integrands have equal totalized real integrals.

\[\int(\sqrt r)^2\,d\pi=\int r\,d\pi=1.\]

Corresponding Lean step

integral_congr_ae

Lean verification

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

Lean proof · lsiKlFiSqrtRnDerivTestMassOne

The proof first imports normalization, then applies integral congruence to a pointwise square-root equality. It supplies no differentiability of the square root.

Download module (.lean)

theorem lsiKlFiSqrtRnDerivTestMassOne {α : Type*} [MeasurableSpace α]
    (rho pi : Measure α) [IsProbabilityMeasure rho] [IsProbabilityMeasure pi]
    (hrho_pi : rho ≪ pi) :
    ∫ x, (Real.sqrt ((rho.rnDeriv pi x).toReal)) ^ 2 ∂pi = 1 := by
  rw [← lsiKlFiRnDerivDensityMassOne rho pi hrho_pi]
  refine integral_congr_ae ?_
  filter_upwards with x
  exact Real.sq_sqrt ENNReal.toReal_nonneg

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

AutoSamplingTheory.lsiKlFiRnDerivDensityMassOne

Mathlib API called (external library)

MeasureTheory.integral_congr_ae
Real.sq_sqrt
ENNReal.toReal_nonneg

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
MeasureTheory.integral_congr_ae — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
Real.sq_sqrt — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
AutoSamplingTheory.lsiKlFiRnDerivDensityMassOne — Existing root ASTIS dependency; use its own adjacent teaching unit.

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