ASTIS mathematical exposition

The square-root density squares back to the density

AutoSamplingTheory.lsiKlFiSqrtDensitySquareScalar · theorem · Teaching coverage

Statement

For every nonnegative real number r, the square of its nonnegative real square root equals r.

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

All objects and hypotheses

r is a real number and hr supplies 0≤r; no measure or density construction is assumed.

Mathematical proof

1. Apply the defining square-root identity

The nonnegativity hypothesis is exactly what the real square-root theorem requires.

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

Corresponding Lean step

Real.sq_sqrt hr

Lean statement · lsiKlFiSqrtDensitySquareScalar

The density interpretation is optional motivation. The formal parameter is only a real number with a nonnegativity proof.

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 lsiKlFiSqrtDensitySquareScalar {r : Real} (hr : 0 ≤ r) :
    (Real.sqrt r) ^ 2 = r

Exact module and namespace context

Lean proof · lsiKlFiSqrtDensitySquareScalar

The proof directly reuses the existing real square-root theorem, without any differentiation or integration.

theorem lsiKlFiSqrtDensitySquareScalar {r : Real} (hr : 0 ≤ r) :
    (Real.sqrt r) ^ 2 = r := by
  exact Real.sq_sqrt hr

/-- Pointwise entropy-integrand rewrite for `phi = sqrt(r)`.

This proves only the scalar rewrite
`phi^2 log(phi^2) = r log r` after nonnegativity of the density ratio is
available.  Integrability, zero-density conventions, and the KL integral
identity are still analytic obligations.
-/

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

Real.sq_sqrt

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.
Real.sq_sqrt — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.

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