Samplinglib mathematical lesson

Rewrite the square-root test's entropy integrand

AutoSamplingTheory.lsiKlFiSqrtDensityEntropyIntegrandScalar · theorem · Teaching coverage

Read this first

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

\[r\ge0\Longrightarrow(\sqrt r)^2\log((\sqrt r)^2)=r\log r.\]

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.

Download module (.lean)

theorem lsiKlFiSqrtDensityEntropyIntegrandScalar {r : Real} (hr : 0 ≤ r) :
    (Real.sqrt r) ^ 2 * Real.log ((Real.sqrt r) ^ 2) = r * Real.log r

Exact module and namespace context

Proof roadmap

1Substitute the square identity in both occurrences
Replace the multiplicative factor and the logarithm's argument by r using the already proved square-root equality.

Full assumptions and notation

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.

\[(\sqrt r)^2=r\Longrightarrow(\sqrt r)^2\log((\sqrt r)^2)=r\log r.\]

Corresponding Lean step

rw [lsiKlFiSqrtDensitySquareScalar hr]

Lean verification

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

Lean proof · lsiKlFiSqrtDensityEntropyIntegrandScalar

A rewrite uses the same equality wherever the squared square root occurs, including inside the logarithm.

Download module (.lean)

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]

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.
No finite-entropy or analytic zero-density admissibility theorem is asserted.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.lsiKlFiSqrtDensitySquareScalar

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib 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.

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