ASTIS mathematical exposition

Name the finite-coordinate Dirichlet and Fisher expressions

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainFiniteSumHandoffScalar · theorem · Teaching coverage

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

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 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.

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

Lean proof · lsiKlFiSqrtDensityFisherChainFiniteSumHandoffScalar

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

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

/-- Integral handoff for the finite-coordinate Fisher chain rule.

After a Sobolev backend supplies coordinate derivative identities almost
everywhere for `sqrt(r)` and `log r`, this pushes the cycle-38 finite-sum
coefficient through the `pi`-integral.  It is still below the full
vector-gradient/Fisher-information theorem: integrability, coordinate-to-vector
gradient equivalence, zero-density handling, and admissibility of `sqrt(r)`
remain separate 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.
Named scalar handoff, not integration or geometric identification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainFiniteSumScalar

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