Samplinglib mathematical lesson

Name the finite-coordinate Dirichlet and Fisher expressions

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainFiniteSumHandoffScalar · theorem · Teaching coverage

Read this first

Mathematical statement

Let I be finite, r>0, and dr,dSqrt,dLog:I→ℝ satisfy the coefficient identities at every coordinate. If real numbers D and J are supplied to equal ∑dSqrt_i² and r∑dLog_i² respectively, then D=J/4.

\[D=\sum_i d_{\sqrt{\ },i}^2,\quad J=r\sum_i d_{\log,i}^2\Longrightarrow D=\tfrac14J.\]

Lean statement · lsiKlFiSqrtDensityFisherChainFiniteSumHandoffScalar

D and J are real values with supplied representations. Their names do not turn them into analytic Dirichlet energy or Fisher information automatically.

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 lsiKlFiSqrtDensityFisherChainFiniteSumHandoffScalar
    {ι : Type*} [Fintype ι] {r dirichlet fisher : Real}
    {dr dSqrt dLog : ι → Real}
    (hr : 0 < r)
    (hdirichlet : dirichlet = ∑ i, dSqrt i ^ 2)
    (hfisher : fisher = r * ∑ i, dLog i ^ 2)
    (hdSqrt : ∀ i, dSqrt i = (1 / (2 * Real.sqrt r)) * dr i)
    (hdLog : ∀ i, dLog i = dr i / r) :
    dirichlet = (1 / 4) * fisher

Exact module and namespace context

Proof roadmap

1Replace the named quantities by their sums
Use the two representation hypotheses to expose the finite-coordinate expressions.
2Reuse the finite-sum identity
The earlier finite-coordinate algebra theorem identifies these expressions.

Full assumptions and notation

All objects and hypotheses

I has Fintype; r,D,J∈ℝ with r>0; dr,dSqrt,dLog:I→ℝ.
D and J have the displayed finite-sum representations, and dSqrt_i=dr_i/(2√r), dLog_i=dr_i/r for every i.

Mathematical proof

1. Replace the named quantities by their sums

Use the two representation hypotheses to expose the finite-coordinate expressions.

\[D=\sum_i d_{\sqrt{\ },i}^2,\quad\tfrac14J=\tfrac14\left(r\sum_i d_{\log,i}^2\right).\]

Corresponding Lean step

rw [hdirichlet,hfisher]

2. Reuse the finite-sum identity

The earlier finite-coordinate algebra theorem identifies these expressions.

\[\sum_i d_{\sqrt{\ },i}^2=\tfrac14\left(r\sum_i d_{\log,i}^2\right).\]

Corresponding Lean step

lsiKlFiSqrtDensityFisherChainFiniteSumScalar hr hdSqrt hdLog

Lean verification

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

Lean proof · lsiKlFiSqrtDensityFisherChainFiniteSumHandoffScalar

Only substitution and the existing finite-sum result are used. No derivative identity or norm representation is established.

Download module (.lean)

theorem lsiKlFiSqrtDensityFisherChainFiniteSumHandoffScalar
    {ι : Type*} [Fintype ι] {r dirichlet fisher : Real}
    {dr dSqrt dLog : ι → Real}
    (hr : 0 < r)
    (hdirichlet : dirichlet = ∑ i, dSqrt i ^ 2)
    (hfisher : fisher = r * ∑ i, dLog i ^ 2)
    (hdSqrt : ∀ i, dSqrt i = (1 / (2 * Real.sqrt r)) * dr i)
    (hdLog : ∀ i, dLog i = dr i / r) :
    dirichlet = (1 / 4) * fisher := by
  rw [hdirichlet, hfisher]
  exact lsiKlFiSqrtDensityFisherChainFiniteSumScalar hr hdSqrt hdLog

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.
Named scalar handoff, not integration or geometric identification.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainFiniteSumScalar

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