Samplinglib mathematical lesson

Sum the scalar Fisher-chain factor over finitely many coordinates

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainFiniteSumScalar · theorem · Teaching coverage

Read this first

Mathematical statement

Let I be a finite index type, r>0 a real number, and dr,dSqrt,dLog:I→ℝ. If at every i the values satisfy dSqrt_i=dr_i/(2√r) and dLog_i=dr_i/r, then the sum of dSqrt_i² is (1/4)r times the sum of dLog_i². The empty finite index type is allowed.

\[\sum_{i\in I}d_{\sqrt{\ },i}^2=\frac14\,r\sum_{i\in I}d_{\log,i}^2.\]

Lean statement · lsiKlFiSqrtDensityFisherChainFiniteSumScalar

Finiteness concerns the coordinate index only. All coordinate derivative formulas are premises, and no inner product or norm is part of the statement.

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

Exact module and namespace context

Proof roadmap

1Prove the identity in each coordinate
Substitute the two supplied formulas at i and apply the scalar theorem.
2Sum equal terms
Equality at each index gives equality of the two finite sums.
3Factor out the common coefficient
Reassociate products, distribute the constant across the finite sum, and reassociate again.

Full assumptions and notation

All objects and hypotheses

I is a type with Fintype; r∈ℝ is strictly positive.
dr,dSqrt,dLog:I→ℝ and the two derivative-coefficient equalities hold for every i.

Mathematical proof

1. Prove the identity in each coordinate

Substitute the two supplied formulas at i and apply the scalar theorem.

\[d_{\sqrt{\ },i}^2=\tfrac14\,r\,d_{\log,i}^2\quad\forall i.\]

Corresponding Lean step

Finset.sum_congr; rw [hdSqrt i,hdLog i]; lsiKlFiSqrtDensityFisherChainScalar hr

2. Sum equal terms

Equality at each index gives equality of the two finite sums.

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

Corresponding Lean step

first calc equality

3. Factor out the common coefficient

Reassociate products, distribute the constant across the finite sum, and reassociate again.

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

Corresponding Lean step

ring; Finset.mul_sum; ring

Lean verification

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

Lean proof · lsiKlFiSqrtDensityFisherChainFiniteSumScalar

The proof checks one summand, replaces the entire finite sum termwise, and pulls out the same scalar coefficient.

Download module (.lean)

theorem lsiKlFiSqrtDensityFisherChainFiniteSumScalar
    {ι : Type*} [Fintype ι] {r : Real} {dr dSqrt dLog : ι → Real}
    (hr : 0 < r)
    (hdSqrt : ∀ i, dSqrt i = (1 / (2 * Real.sqrt r)) * dr i)
    (hdLog : ∀ i, dLog i = dr i / r) :
    (∑ i, dSqrt i ^ 2) = (1 / 4) * (r * ∑ i, dLog i ^ 2) := by
  calc
    (∑ i, dSqrt i ^ 2) = ∑ i, (1 / 4) * (r * dLog i ^ 2) := by
      refine Finset.sum_congr rfl ?_
      intro i _hi
      rw [hdSqrt i, hdLog i]
      exact lsiKlFiSqrtDensityFisherChainScalar hr
    _ = ∑ i, ((1 / 4) * r) * dLog i ^ 2 := by
      refine Finset.sum_congr rfl ?_
      intro i _hi
      ring
    _ = ((1 / 4) * r) * ∑ i, dLog i ^ 2 := by
      rw [Finset.mul_sum]
    _ = (1 / 4) * (r * ∑ i, dLog i ^ 2) := by
      ring

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.
A coordinate-square sum is not automatically the squared norm of a gradient; an application must justify that identification.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainScalar

Mathlib API called (external library)

Finset.sum_congr
Finset.mul_sum

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.

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