theorem
Verification.integral_tensor_square
{α : Type u_1}
{β : Type u_2}
[Fintype α]
[Fintype β]
(D : α → β → ℝ)
(f : α → C(↑unitInterval, ℝ))
(g : β → C(↑unitInterval, ℝ))
:
∫ (v : ↑unitInterval) (u : ↑unitInterval), (∑ i : α, ∑ j : β, D i j * (f i) u * (g j) v) ^ 2 = ∑ i : α,
∑ j : β,
∑ r : α,
∑ s : β, (D i j * D r s * ∫ (u : ↑unitInterval), (f i) u * (f r) u) * ∫ (v : ↑unitInterval), (g j) v * (g s) v
Squared tensor expansions integrate into the contraction of two Gram matrices.