Bilinear forms on finite linear combinations and Euclidean inner products #
A scalar-valued bilinear form evaluated on the finite linear combinations ∑ k, f i k • φ k and
∑ l, g i l • ψ l, summed over i, is the matrix sum ∑ k, ∑ l, B (φ k) (ψ l) * ⟪u k, v l⟫
for the Euclidean vectors u k = (conj (f i k))ᵢ and v l = (g i l)ᵢ.
Main results #
LinearMap.sum_apply_sum_smul_sum_smul_eq: the identity.
theorem
LinearMap.sum_apply_sum_smul_sum_smul_eq
{𝕜 : Type u_1}
{ι : Type u_2}
[RCLike 𝕜]
[Fintype ι]
{M : Type u_3}
{N : Type u_4}
[AddCommMonoid M]
[Module 𝕜 M]
[AddCommMonoid N]
[Module 𝕜 N]
{s : Type u_5}
{t : Type u_6}
[Fintype s]
[Fintype t]
(B : M →ₗ[𝕜] N →ₗ[𝕜] 𝕜)
(φ : s → M)
(ψ : t → N)
(f : ι → s → 𝕜)
(g : ι → t → 𝕜)
:
∑ k : s,
∑ l : t,
(B (φ k)) (ψ l) * inner 𝕜 (WithLp.toLp 2 fun (i : ι) => star (f i k)) (WithLp.toLp 2 fun (i : ι) => g i l) = ∑ i : ι, (B (∑ k : s, f i k • φ k)) (∑ l : t, g i l • ψ l)
Expanding the finite linear combinations ∑ k, f i k • φ k and ∑ l, g i l • ψ l in a
bilinear form turns ∑ i, B (∑ k, f i k • φ k) (∑ l, g i l • ψ l) into the matrix sum
∑ k, ∑ l, B (φ k) (ψ l) * ⟪u k, v l⟫ for the Euclidean vectors u k = (conj (f i k))ᵢ and
v l = (g i l)ᵢ.