Finite products of absolutely convergent series

This small utility expands a finite product of tsums as one tsum over mode assignments. It is the deterministic Fubini lemma needed to turn a product of cutoff covariances into a countable Fourier configuration sum.

def Anderson4D.finSeriesAssignmentTerm {A : Type u_1} (n : ℕ) (f : Fin n → A → ℂ) (q : Fin n → A) : ℂ

Product of one term from each of n series.

Equations

• Anderson4D.finSeriesAssignmentTerm n f q = ∏ i : Fin n, f i (q i)

theorem Anderson4D.summable_norm_finSeriesAssignmentTerm {A : Type u_1} (n : ℕ) (f : Fin n → A → ℂ) (hf : ∀ (i : Fin n), Summable fun (a : A) => ‖f i a‖) : Summable fun (q : Fin n → A) => ‖finSeriesAssignmentTerm n f q‖

Absolute convergence is preserved when finitely many series are expanded over all assignments of their indices.

theorem Anderson4D.summable_finSeriesAssignmentTerm {A : Type u_1} (n : ℕ) (f : Fin n → A → ℂ) (hf : ∀ (i : Fin n), Summable fun (a : A) => ‖f i a‖) : Summable (finSeriesAssignmentTerm n f)

In particular the finite assignment series itself is summable.

theorem Anderson4D.tsum_finSeriesAssignmentTerm {A : Type u_1} (n : ℕ) (f : Fin n → A → ℂ) (hf : ∀ (i : Fin n), Summable fun (a : A) => ‖f i a‖) : ∑' (q : Fin n → A), finSeriesAssignmentTerm n f q = ∏ i : Fin n, ∑' (a : A), f i a

A finite product of tsums is the tsum over all finite mode assignments.