ASTIS mathematical exposition

Transfer a supplied unit-mass identity

AutoSamplingTheory.lsiKlFiSqrtDensityNormalizationScalar · theorem · Teaching coverage

Statement

Let densityMass and testMass be real numbers. If testMass=densityMass and densityMass=1, then testMass=1. Their names carry no measure-theoretic meaning unless an application supplies it.

\[\text{testMass}=\text{densityMass},\quad\text{densityMass}=1\Longrightarrow\text{testMass}=1.\]

All objects and hypotheses

densityMass,testMass∈ℝ; the two displayed equalities are supplied.

Mathematical proof

1. Chain the given equalities

Replace testMass by densityMass, and then replace densityMass by one.

\[\text{testMass}=\text{densityMass}=1.\]

Corresponding Lean step

rw [htest,hdensity]

Lean statement · lsiKlFiSqrtDensityNormalizationScalar

The two inputs are arbitrary real numbers. Equalities connecting them to actual integrals are not part of this theorem.

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 lsiKlFiSqrtDensityNormalizationScalar {densityMass testMass : Real}
    (htest : testMass = densityMass)
    (hdensity : densityMass = 1) :
    testMass = 1

Exact module and namespace context

Lean proof · lsiKlFiSqrtDensityNormalizationScalar

The proof uses transitivity by rewriting; it does not calculate density mass or establish probability normalization.

theorem lsiKlFiSqrtDensityNormalizationScalar {densityMass testMass : Real}
    (htest : testMass = densityMass)
    (hdensity : densityMass = 1) :
    testMass = 1 := by
  rw [htest, hdensity]

/-- Radon-Nikodym mass normalization for the LSI density ratio.

For probability measures `rho << pi`, the density ratio `d rho / d pi` has
unit `pi`-mass.  This is the measure-level backend behind the source line
`int phi^2 d pi = int (rho/pi) d pi = 1` before converting to real integrals.
-/

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.
This is an equality handoff, not a normalization theorem for any measure.

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.

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