ASTIS mathematical exposition

Rewrite the square-root test entropy as a log-likelihood integral

AutoSamplingTheory.lsiKlFiSqrtRnDerivEntropyIntegral · theorem · Teaching coverage

Statement

For probability measures ρ≪π and r=(dρ/dπ).toReal, the real integral of (√r)² log((√r)²) under π equals the integral of llr(ρ,π) under ρ. No finite-entropy or test-admissibility claim is made.

\[\int(\sqrt r)^2\log((\sqrt r)^2)\,d\pi=\int\ell_{\rho,\pi}\,d\rho.\]

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. Use the established density-entropy transport

Replace the log-likelihood integral by ∫r log r dπ.

\[\int\ell_{\rho,\pi}\,d\rho=\int r\log r\,d\pi.\]

Corresponding Lean step

rw [← lsiKlFiRnDerivEntropyIntegral rho pi hrho_pi]

2. Rewrite each nonnegative density value

At every x, nonnegativity of r(x) gives the scalar square-root entropy identity.

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

Corresponding Lean step

lsiKlFiSqrtDensityEntropyIntegrandScalar ENNReal.toReal_nonneg

3. Integrate the a.e. equality

Pointwise equality supplies the a.e. congruence required for equal real integrals.

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

Corresponding Lean step

integral_congr_ae

Lean statement · lsiKlFiSqrtRnDerivEntropyIntegral

This substitutes a particular square-root density into an integrand. It does not certify that this function belongs to an LSI's admissible class.

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

Exact module and namespace context

Lean proof · lsiKlFiSqrtRnDerivEntropyIntegral

The proof combines one previously established measure-transport identity with a pointwise algebraic rewrite and integral congruence.

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

/-- One-dimensional pointwise Fisher-chain coefficient for the LSI test.

For a positive density ratio `r`, the source substitution
`phi=sqrt(r)` has differential coefficient
`d phi = (2*sqrt(r))^{-1} d r`, while
`d log r = r^{-1} d r`.  This scalar lemma proves the resulting
`1/4` factor in the Fisher integrand.  The vector-gradient and integral
versions remain separate analytic obligations.
-/

Exact module and namespace context

Scope and omitted-condition boundaries

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

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.integral_congr_ae
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.
AutoSamplingTheory.lsiKlFiRnDerivEntropyIntegral — Existing root ASTIS dependency; use its own adjacent teaching unit.
AutoSamplingTheory.lsiKlFiSqrtDensityEntropyIntegrandScalar — 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.