Comparing linear combinations by their Gram kernels #
Two families with the same pairwise inner products give linear combinations of the same norm when supplied with the same finitely supported coefficients. This comparison applies in seminormed inner product spaces and is useful for comparing realizations of a positive-definite kernel before constructing an isometry between their closed spans.
theorem
Finsupp.norm_linearCombination_eq_of_inner_eq
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{F : Type u_4}
[RCLike 𝕜]
[SeminormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[SeminormedAddCommGroup F]
[InnerProductSpace 𝕜 F]
(f : α →₀ 𝕜)
{φ : α → E}
{ψ : α → F}
(h : ∀ (a b : α), inner 𝕜 (φ a) (φ b) = inner 𝕜 (ψ a) (ψ b))
:
Families with equal pairwise inner products give linear combinations of equal norm for the same finitely supported coefficients.