Amplification of operators to a finite Hilbert sum

For a Hilbert space H over ℝ or ℂ and a finite index type ι, an operator s on H acts diagonally on the Hilbert sum PiLp 2 (fun _ : ι => H) of copies of H, as s ⊕ ⋯ ⊕ s. This diagonal amplification is a star algebra homomorphism, PiLp.diagStarAlgHom. Conversely, every operator T on the Hilbert sum has matrix entries ContinuousLinearMap.piLpEntry T i j : H →L[𝕜] H, and T acts through them (ContinuousLinearMap.apply_eq_sum_piLpEntry). The amplification of s has s on the diagonal and 0 off it (ContinuousLinearMap.piLpEntry_diagStarAlgHom).

Amplification turns statements about finitely many vectors of H into statements about a single vector of the Hilbert sum; this is how the von Neumann density theorem passes from one vector to finitely many.

noncomputable def ContinuousLinearMap.piLpEntry {𝕜 : Type u_1} {H : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [DecidableEq ι] (T : (PiLp 2 fun (x : ι) => H) →L[𝕜] PiLp 2 fun (x : ι) => H) (i j : ι) : H →L[𝕜] H

The (i, j) matrix entry of an operator on the Hilbert sum of copies of H: the component at i of the image of a vector supported at j.

@[simp]

theorem ContinuousLinearMap.piLpEntry_apply {𝕜 : Type u_1} {H : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [DecidableEq ι] (T : (PiLp 2 fun (x : ι) => H) →L[𝕜] PiLp 2 fun (x : ι) => H) (i j : ι) (h : H) : (T.piLpEntry i j) h = (T (PiLp.single 2 j h)).ofLp i

theorem ContinuousLinearMap.apply_eq_sum_piLpEntry {𝕜 : Type u_1} {H : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [DecidableEq ι] [Fintype ι] (T : (PiLp 2 fun (x : ι) => H) →L[𝕜] PiLp 2 fun (x : ι) => H) (w : PiLp 2 fun (x : ι) => H) (i : ι) : (T w).ofLp i = ∑ j : ι, (T.piLpEntry i j) (w.ofLp j)

An operator on the Hilbert sum acts through its matrix entries.

noncomputable def PiLp.diagStarAlgHom (𝕜 : Type u_1) (H : Type u_2) (ι : Type u_3) [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Fintype ι] [CompleteSpace H] : (H →L[𝕜] H) →⋆ₐ[𝕜] (PiLp 2 fun (x : ι) => H) →L[𝕜] PiLp 2 fun (x : ι) => H

The diagonal amplification s ↦ s ⊕ ⋯ ⊕ s of operators on H to the Hilbert sum of copies of H indexed by ι, as a star algebra homomorphism.

@[simp]

theorem PiLp.diagStarAlgHom_apply {𝕜 : Type u_1} {H : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Fintype ι] [CompleteSpace H] (s : H →L[𝕜] H) (w : PiLp 2 fun (x : ι) => H) (i : ι) : (((diagStarAlgHom 𝕜 H ι) s) w).ofLp i = s (w.ofLp i)

@[simp]

theorem PiLp.diagStarAlgHom_apply_single {𝕜 : Type u_1} {H : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Fintype ι] [CompleteSpace H] [DecidableEq ι] (s : H →L[𝕜] H) (j : ι) (h : H) : ((diagStarAlgHom 𝕜 H ι) s) (single 2 j h) = single 2 j (s h)

theorem ContinuousLinearMap.piLpEntry_diagStarAlgHom {𝕜 : Type u_1} {H : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Fintype ι] [DecidableEq ι] [CompleteSpace H] (s : H →L[𝕜] H) (i j : ι) : ((PiLp.diagStarAlgHom 𝕜 H ι) s).piLpEntry i j = if i = j then s else 0

The diagonal amplification of s has s on the diagonal and 0 off it.