Inner products of linear combinations

A general identity expanding the inner product of two finite linear combinations of a vector family over the family's pairwise inner products ⟪v i, v j⟫. It involves no orthonormality, no Gram matrix, and no rigidity hypothesis; it is the reusable algebraic core behind the Gram-rigidity development in Mathlib/Analysis/InnerProductSpace/GramMatrix.lean, and belongs next to Finsupp.sum_inner / Finsupp.inner_sum.

Main results

• TauCeti.inner_linearCombination_linearCombination: expands ⟪Σ aᵢ • v i, Σ bⱼ • v j⟫ as Σᵢ Σⱼ conj aᵢ * bⱼ * ⟪v i, v j⟫.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib.Analysis.InnerProductSpace.Basic, moved to ForTauCeti in the Wave-1 staging migration; introduced at Davis--Kahan commit 6d8c37c.
• Extraction class: moved. The Wave-1 migration renamed the namespace ForMathlib to TauCeti; declaration names and proofs are unchanged.
• Original authors / copyright: Jon Crall, Claude Fable 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

theorem TauCeti.inner_linearCombination_linearCombination {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : ι → E) (a b : ι →₀ 𝕜) : inner 𝕜 ((Finsupp.linearCombination 𝕜 v) a) ((Finsupp.linearCombination 𝕜 v) b) = a.sum fun (i : ι) (s : 𝕜) => b.sum fun (j : ι) (t : 𝕜) => (starRingEnd 𝕜) s * t * inner 𝕜 (v i) (v j)

The inner product of two finite linear combinations Σ aᵢ • v i and Σ bⱼ • v j of a vector family v, expanded over the family's Gram data ⟪v i, v j⟫: ⟪Σ aᵢ • vᵢ, Σ bⱼ • vⱼ⟫ = Σᵢ Σⱼ conj aᵢ * bⱼ * ⟪vᵢ, vⱼ⟫.