Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

Sum the scalar Fisher-chain factor over finitely many coordinates

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainFiniteSumScalar · theorem · Teaching coverage

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

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

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

Lean proof · lsiKlFiSqrtDensityFisherChainFiniteSumScalar

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

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

/-- Finite-coordinate handoff to the Dirichlet/Fisher identity.

Once a density backend identifies the Dirichlet term with the finite coordinate
sum of `d sqrt(r)` squares and the Fisher term with
`r * sum_i (d log r_i)^2`, this lemma supplies the exact
`dirichlet = (1/4)*FI` input consumed by the existing LSI/KL/FI scalar bridge.
It does not construct the Radon--Nikodym density, prove differentiability, or
integrate the identity.
-/

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • Finset.sum_congr
  • Finset.mul_sum

Mathematical sources

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