Integral formula for Hilbert-valued contraction

The adjoint definition of tensor contraction is identified with its literal finite-spin integral formula after pairing against an arbitrary target vector. For an L² target, the second theorem expands that target pairing as the nested integral over its representatives.

theorem LiebThirring.inner_tensorContraction {ι : Type u_1} {α : Type u_2} {H : Type u_3} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) (ψ : ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => H) 2 μ)) (v : H) : inner ℂ v ((tensorContraction f) ψ) = ∫ (x : α), ∑ s : ι, (starRingEnd ((fun (x : ι) => ℂ) s)) ((↑↑f x).ofLp s) * inner ℂ v ((↑↑ψ x).ofLp s) ∂μ

Weak integral formula for tensor contraction. Since the test vector is arbitrary, this identity uniquely determines the contracted Hilbert vector.