Samplinglib mathematical lesson

Transfer a supplied unit-mass identity

AutoSamplingTheory.lsiKlFiSqrtDensityNormalizationScalar · theorem · Teaching coverage

Read this first

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

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.

Download module (.lean)

theorem lsiKlFiSqrtDensityNormalizationScalar {densityMass testMass : Real}
    (htest : testMass = densityMass)
    (hdensity : densityMass = 1) :
    testMass = 1

Exact module and namespace context

Proof roadmap

1Chain the given equalities
Replace testMass by densityMass, and then replace densityMass by one.

Full assumptions and notation

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 verification

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

Lean proof · lsiKlFiSqrtDensityNormalizationScalar

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

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

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.

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