Rewrite the square-root test's entropy integrand
AutoSamplingTheory.lsiKlFiSqrtDensityEntropyIntegrandScalar · theorem · Teaching coverage
Statement
For every real r≥0, the expression (√r)² log((√r)²) equals r log r, using Mathlib's real logarithm convention, including its value at zero.
All objects and hypotheses
- r∈ℝ and 0≤r. The real logarithm is totalized; Real.log 0=0, so the displayed identity includes r=0.
Mathematical proof
1. Substitute the square identity in both occurrences
Replace the multiplicative factor and the logarithm's argument by r using the already proved square-root equality.
Corresponding Lean step
rw [lsiKlFiSqrtDensitySquareScalar hr]
Lean statement · lsiKlFiSqrtDensityEntropyIntegrandScalar
The theorem is equality of two real numbers. It does not assume or assert that either expression is integrable under any measure.
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 lsiKlFiSqrtDensityEntropyIntegrandScalar {r : Real} (hr : 0 ≤ r) :
(Real.sqrt r) ^ 2 * Real.log ((Real.sqrt r) ^ 2) = r * Real.log rLean proof · lsiKlFiSqrtDensityEntropyIntegrandScalar
A rewrite uses the same equality wherever the squared square root occurs, including inside the logarithm.
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 lsiKlFiSqrtDensityEntropyIntegrandScalar {r : Real} (hr : 0 ≤ r) :
(Real.sqrt r) ^ 2 * Real.log ((Real.sqrt r) ^ 2) = r * Real.log r := by
rw [lsiKlFiSqrtDensitySquareScalar hr]
/-- Scalar normalization handoff for the LSI test `phi = sqrt(r)`.
After an integral backend has shown that the mass of `phi^2` equals the mass of
the density ratio `r`, probability normalization of `r` gives the LSI test
normalization. This does not prove the integral equality itself.
-/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 finite-entropy or analytic zero-density admissibility theorem is asserted.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
No direct Mathlib call recorded; see the ASTIS parents.
Mathematical sources
- Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
- Existing source-facing LSI context — Local comment cites SALD main_body.tex:208–215; no new primary-source inspection or fidelity verdict.
- AutoSamplingTheory.lsiKlFiSqrtDensitySquareScalar — 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.