Amplification x ↦ x ⊕ ⋯ ⊕ x

theorem Orthogonalization.MvN.amplify_apply_coord {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (n : ℕ) (x : H →L[ℂ] H) (w : FinDim.BlockSpace H (Fin n)) (j : Fin n) : ((amplify n x) w).ofLp j = x (w.ofLp j)

theorem Orthogonalization.MvN.proj_amplify {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (x : H →L[ℂ] H) (i : Fin n) (w : FinDim.BlockSpace H (Fin n)) : (FinDim.proj i) ((amplify n x) w) = x ((FinDim.proj i) w)

theorem Orthogonalization.MvN.amplify_embed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (x : H →L[ℂ] H) (i : Fin n) (v : H) : (amplify n x) ((FinDim.embed i) v) = (FinDim.embed i) (x v)

theorem Orthogonalization.MvN.amplify_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (n : ℕ) (x y : H →L[ℂ] H) : amplify n (x * y) = amplify n x * amplify n y

theorem Orthogonalization.MvN.amplify_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (n : ℕ) : amplify n 1 = 1

theorem Orthogonalization.MvN.amplify_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (n : ℕ) : amplify n 0 = 0

theorem Orthogonalization.MvN.amplify_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (n : ℕ) (x y : H →L[ℂ] H) : amplify n (x + y) = amplify n x + amplify n y

theorem Orthogonalization.MvN.amplify_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (n : ℕ) (x y : H →L[ℂ] H) : amplify n (x - y) = amplify n x - amplify n y

theorem Orthogonalization.MvN.amplify_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (n : ℕ) (c : ℂ) (x : H →L[ℂ] H) : amplify n (c • x) = c • amplify n x

theorem Orthogonalization.MvN.amplify_sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (n : ℕ) {κ : Type u_2} (s : Finset κ) (x : κ → H →L[ℂ] H) : amplify n (∑ k ∈ s, x k) = ∑ k ∈ s, amplify n (x k)

theorem Orthogonalization.MvN.amplify_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (n : ℕ) (x : H →L[ℂ] H) : amplify n (star x) = star (amplify n x)

theorem Orthogonalization.MvN.isStarProjection_amplify {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {p : H →L[ℂ] H} (hp : IsStarProjection p) : IsStarProjection (amplify n p)

Membership in M_n(M) as commutation with the amplified commutant

theorem Orthogonalization.MvN.mem_matrixAlgebra_iff_mem_centralizer {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} {X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)} : X ∈ matrixAlgebra M n ↔ X ∈ StarSubalgebra.centralizer ℂ (Set.range fun (y : ↥M.commutant) => amplify n ↑y)

Membership in M_n(M), unfolded (matrixAlgebra is the centralizer of the amplified commutant {y ⊕ ⋯ ⊕ y | y ∈ M'}).

theorem Orthogonalization.MvN.mem_matrixAlgebra_iff_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} {X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)} : X ∈ matrixAlgebra M n ↔ ∀ y ∈ M.commutant, amplify n y * X = X * amplify n y

X ∈ M_n(M) iff X commutes with the amplification of every y ∈ M' (the star condition of the centralizer is the same one for star y ∈ M').

theorem Orthogonalization.MvN.amplify_mul_eq_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} {X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)} (hX : X ∈ matrixAlgebra M n) {y : H →L[ℂ] H} (hy : y ∈ M.commutant) : amplify n y * X = X * amplify n y

theorem Orthogonalization.MvN.amplify_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} {x : H →L[ℂ] H} (hx : x ∈ M) : amplify n x ∈ matrixAlgebra M n

M ∋ x ↦ x ⊕ ⋯ ⊕ x ∈ M_n(M).

Block entries

theorem Orthogonalization.MvN.entry_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i j : Fin n) (v : H) : (entry X i j) v = (FinDim.proj i) (X ((FinDim.embed j) v))

theorem Orthogonalization.MvN.apply_coord_eq_sum_entry {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (w : FinDim.BlockSpace H (Fin n)) (i : Fin n) : (X w).ofLp i = ∑ j : Fin n, (entry X i j) (w.ofLp j)

Coordinate i of X w is ∑ⱼ X_{ij} (w j).

theorem Orthogonalization.MvN.eq_sum_embed_entry_proj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) : X = ∑ i : Fin n, ∑ j : Fin n, FinDim.embed i ∘SL entry X i j ∘SL FinDim.proj j

X = ∑ᵢⱼ embed i ∘ X_{ij} ∘ proj j.

theorem Orthogonalization.MvN.entry_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (i j : Fin n) : entry 0 i j = 0

theorem Orthogonalization.MvN.entry_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (i j : Fin n) : entry 1 i j = if i = j then 1 else 0

theorem Orthogonalization.MvN.entry_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (X Y : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i j : Fin n) : entry (X + Y) i j = entry X i j + entry Y i j

theorem Orthogonalization.MvN.entry_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (X Y : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i j : Fin n) : entry (X - Y) i j = entry X i j - entry Y i j

theorem Orthogonalization.MvN.entry_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (c : ℂ) (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i j : Fin n) : entry (c • X) i j = c • entry X i j

theorem Orthogonalization.MvN.entry_sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} {κ : Type u_2} (s : Finset κ) (X : κ → FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i j : Fin n) : entry (∑ k ∈ s, X k) i j = ∑ k ∈ s, entry (X k) i j

theorem Orthogonalization.MvN.entry_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (X Y : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i j : Fin n) : entry (X * Y) i j = ∑ k : Fin n, entry X i k * entry Y k j

(XY)_{ij} = ∑ₖ X_{ik} Y_{kj}.

theorem Orthogonalization.MvN.entry_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i j : Fin n) : entry (star X) i j = star (entry X j i)

(X*)_{ij} = (X_{ji})*.

theorem Orthogonalization.MvN.entry_amplify {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (x : H →L[ℂ] H) (i j : Fin n) : entry (amplify n x) i j = if i = j then x else 0

theorem Orthogonalization.MvN.entry_blockProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (q : Fin n → H →L[ℂ] H) (i j : Fin n) : entry (FinDim.blockProj q) i j = if i = j then q i else 0

theorem Orthogonalization.MvN.entry_blockMap_comp_proj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (X : Fin n → H →L[ℂ] H) (k i j : Fin n) : entry (FinDim.blockMap X ∘SL FinDim.proj k) i j = if k = j then X i else 0

The entries of the "column" matrix blockMap X ∘ proj k, with X i in column k.

The membership criterion: X ∈ M_n(M) ↔ ∀ i j, X_{ij} ∈ M

theorem Orthogonalization.MvN.entry_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} {X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)} (hX : X ∈ matrixAlgebra M n) (i j : Fin n) : entry X i j ∈ M

The entries of an element of M_n(M) lie in M: they commute with every y ∈ M' because X commutes with y ⊕ ⋯ ⊕ y.

theorem Orthogonalization.MvN.mem_matrixAlgebra_of_entry {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} {X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)} (h : ∀ (i j : Fin n), entry X i j ∈ M) : X ∈ matrixAlgebra M n

An operator on H^n whose entries lie in M is in M_n(M).

theorem Orthogonalization.MvN.mem_matrixAlgebra_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} {X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)} : X ∈ matrixAlgebra M n ↔ ∀ (i j : Fin n), entry X i j ∈ M

The membership criterion: X ∈ M_n(M) ↔ ∀ i j, X_{ij} ∈ M.

theorem Orthogonalization.MvN.blockProj_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} {q : Fin n → H →L[ℂ] H} (hq : ∀ (i : Fin n), q i ∈ M) : FinDim.blockProj q ∈ matrixAlgebra M n

A diagonal matrix with entries in M lies in M_n(M).

theorem Orthogonalization.MvN.blockMap_comp_proj_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} {X : Fin n → H →L[ℂ] H} (hX : ∀ (i : Fin n), X i ∈ M) (k : Fin n) : FinDim.blockMap X ∘SL FinDim.proj k ∈ matrixAlgebra M n

A "column" matrix blockMap X ∘ proj k with entries in M lies in M_n(M).

V* V and V V* read blockwise

theorem Orthogonalization.MvN.entry_star_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (V : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i j : Fin n) : entry (star V * V) i j = ∑ k : Fin n, star (entry V k i) * entry V k j

(V* V)_{ij} = ∑ₖ (V_{ki})* V_{kj}.

theorem Orthogonalization.MvN.entry_mul_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (V : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i j : Fin n) : entry (V * star V) i j = ∑ k : Fin n, entry V i k * star (entry V j k)

(V V*)_{ij} = ∑ₖ V_{ik} (V_{jk})*.

Diagonal trace helpers

theorem Orthogonalization.MvN.sum_entry_mul_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) (hE : ∀ x ∈ M, ∀ y ∈ M, E (x * y) = E (y * x)) {X Y : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)} (hX : ∀ (i j : Fin n), entry X i j ∈ M) (hY : ∀ (i j : Fin n), entry Y i j ∈ M) : ∑ i : Fin n, E (entry (X * Y) i i) = ∑ i : Fin n, E (entry (Y * X) i i)

The diagonal sum X ↦ ∑ᵢ E(Xᵢᵢ) of a tracial E on M is tracial on the matrices with entries in M: ∑ᵢ E((XY)ᵢᵢ) = ∑ᵢ E((YX)ᵢᵢ).

theorem Orthogonalization.MvN.sum_entry_star_mul_self_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) (hE : ∀ x ∈ M, ∀ y ∈ M, E (x * y) = E (y * x)) {V : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)} (hV : ∀ (i j : Fin n), entry V i j ∈ M) : ∑ i : Fin n, E (entry (star V * V) i i) = ∑ i : Fin n, E (entry (V * star V) i i)

∑ᵢ E((V* V)ᵢᵢ) = ∑ᵢ E((V V*)ᵢᵢ) for a tracial E on M and V with entries in M.