The squared square-root Radon–Nikodym test has unit mass
AutoSamplingTheory.lsiKlFiSqrtRnDerivTestMassOne · theorem · Teaching coverage
Statement
For probability measures ρ≪π and r=(dρ/dπ).toReal, the real integral of (√r)² against π is one.
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.
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.
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.
Corresponding Lean step
integral_congr_ae
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.
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 = 1Lean 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.
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 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
/-- Entropy transport from the density-ratio integral to the KL log-likelihood integral.
For `rho << pi`, Mathlib's log-likelihood-ratio backend identifies
`int (d rho/d pi) log(d rho/d pi) d pi` with the paper's KL integrand
`int log(d rho/d pi) d rho`. Finite-KL assumptions for theorem use remain
explicit downstream.
-/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.
Source and reuse
ASTIS parents called
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.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.