ASTIS mathematical exposition

Apply the scalar coefficient identity to supplied derivative values

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainOfDerivativesScalar · theorem · Teaching coverage

Statement

Let r>0 and dr,dSqrt,dLog be real numbers. If dSqrt=dr/(2√r) and dLog=dr/r, then dSqrt²=(1/4)r dLog². The named derivative identities are explicit assumptions.

\[d_{\sqrt{\ }}=\frac{dr}{2\sqrt r},\quad d_{\log}=\frac{dr}{r}\Longrightarrow d_{\sqrt{\ }}^2=\tfrac14\,r\,d_{\log}^2.\]

All objects and hypotheses

r,dr,dSqrt,dLog∈ℝ with r>0.
The two coefficient identities for dSqrt and dLog are supplied; no functions or differentiability hypotheses are inferred from their names.

Mathematical proof

1. Substitute the supplied identities

Replace each named derivative value by its explicit scalar coefficient expression.

\[d_{\sqrt{\ }}^2=\left(\frac{dr}{2\sqrt r}\right)^2,\quad r\,d_{\log}^2=r\left(\frac{dr}{r}\right)^2.\]

Corresponding Lean step

rw [hdSqrt,hdLog]

2. Reuse the scalar algebra theorem

The previous positive-r identity supplies the required factor one quarter.

\[\left(\frac{dr}{2\sqrt r}\right)^2=\tfrac14r\left(\frac{dr}{r}\right)^2.\]

Corresponding Lean step

lsiKlFiSqrtDensityFisherChainScalar hr

Lean statement · lsiKlFiSqrtDensityFisherChainOfDerivativesScalar

This handoff takes values called derivatives plus formulas for them. It does not prove a chain rule for any underlying function.

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 lsiKlFiSqrtDensityFisherChainOfDerivativesScalar
    {r dr dSqrt dLog : Real}
    (hr : 0 < r)
    (hdSqrt : dSqrt = (1 / (2 * Real.sqrt r)) * dr)
    (hdLog : dLog = dr / r) :
    dSqrt ^ 2 = (1 / 4) * (r * dLog ^ 2)

Exact module and namespace context

Lean proof · lsiKlFiSqrtDensityFisherChainOfDerivativesScalar

After substituting the two premises, the goal is exactly the preceding scalar theorem.

theorem lsiKlFiSqrtDensityFisherChainOfDerivativesScalar
    {r dr dSqrt dLog : Real}
    (hr : 0 < r)
    (hdSqrt : dSqrt = (1 / (2 * Real.sqrt r)) * dr)
    (hdLog : dLog = dr / r) :
    dSqrt ^ 2 = (1 / 4) * (r * dLog ^ 2) := by
  rw [hdSqrt, hdLog]
  exact lsiKlFiSqrtDensityFisherChainScalar hr

/-- Finite-coordinate Fisher-chain handoff for the LSI density test.

This lifts the pointwise scalar identity for `phi=sqrt(r)` to a finite sum of
coordinate-square terms.  It is still not the vector Sobolev chain rule or the
integral identity for Fisher information; those analytic backends must supply
the coordinate derivative identities and the later integral transport.
-/

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

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainScalar

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.
AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainScalar — 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.