Extensionality by entries

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

Two operators on H^n with the same entries are equal.

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

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

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

The entries of an operator X = (1_n ⊗ p) X (1_n ⊗ p) lie in the corner p M p.

The algebra of block-diagonal operators

theorem Orthogonalization.MvN.blockProj_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (q q' : Fin n → H →L[ℂ] H) : FinDim.blockProj q * FinDim.blockProj q' = FinDim.blockProj fun (i : Fin n) => q i * q' i

theorem Orthogonalization.MvN.blockProj_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} : (FinDim.blockProj fun (x : Fin n) => 0) = 0

theorem Orthogonalization.MvN.blockProj_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} : (FinDim.blockProj fun (x : Fin n) => 1) = 1

theorem Orthogonalization.MvN.blockProj_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (q q' : Fin n → H →L[ℂ] H) : (FinDim.blockProj fun (i : Fin n) => q i + q' i) = FinDim.blockProj q + FinDim.blockProj q'

theorem Orthogonalization.MvN.blockProj_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (q q' : Fin n → H →L[ℂ] H) : (FinDim.blockProj fun (i : Fin n) => q i - q' i) = FinDim.blockProj q - FinDim.blockProj q'

theorem Orthogonalization.MvN.blockProj_sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {κ : Type u_2} (s : Finset κ) (q : κ → Fin n → H →L[ℂ] H) : (FinDim.blockProj fun (i : Fin n) => ∑ k ∈ s, q k i) = ∑ k ∈ s, FinDim.blockProj (q k)

theorem Orthogonalization.MvN.blockProj_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (q : Fin n → H →L[ℂ] H) : star (FinDim.blockProj q) = FinDim.blockProj fun (i : Fin n) => star (q i)

theorem Orthogonalization.MvN.isStarProjection_blockProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {q : Fin n → H →L[ℂ] H} (h : ∀ (i : Fin n), IsStarProjection (q i)) : IsStarProjection (FinDim.blockProj q)

theorem Orthogonalization.MvN.blockProj_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {q : Fin n → H →L[ℂ] H} (h : ∀ (i : Fin n), 0 ≤ q i) : 0 ≤ FinDim.blockProj q

theorem Orthogonalization.MvN.blockProj_le_blockProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {q q' : Fin n → H →L[ℂ] H} (h : ∀ (i : Fin n), q i ≤ q' i) : FinDim.blockProj q ≤ FinDim.blockProj q'

theorem Orthogonalization.MvN.blockProj_inj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {q q' : Fin n → H →L[ℂ] H} (h : FinDim.blockProj q = FinDim.blockProj q') : q = q'

theorem Orthogonalization.MvN.amplify_mul_blockProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (x : H →L[ℂ] H) (q : Fin n → H →L[ℂ] H) : amplify n x * FinDim.blockProj q = FinDim.blockProj fun (i : Fin n) => x * q i

theorem Orthogonalization.MvN.blockProj_mul_amplify {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (q : Fin n → H →L[ℂ] H) (x : H →L[ℂ] H) : FinDim.blockProj q * amplify n x = FinDim.blockProj fun (i : Fin n) => q i * x

Single-block operators e_{ii} ⊗ x

noncomputable def Orthogonalization.MvN.single {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (i : Fin n) (x : H →L[ℂ] H) : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)

The operator e_{ii} ⊗ x on H^n: x in the (i, i) block, zero elsewhere.

Equations

• Orthogonalization.MvN.single i x = Orthogonalization.FinDim.blockProj fun (j : Fin n) => if j = i then x else 0

theorem Orthogonalization.MvN.single_apply_coord {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (i : Fin n) (x : H →L[ℂ] H) (w : FinDim.BlockSpace H (Fin n)) (j : Fin n) : ((single i x) w).ofLp j = if j = i then x (w.ofLp j) else 0

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

theorem Orthogonalization.MvN.entry_single_same {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (i : Fin n) (x : H →L[ℂ] H) : entry (single i x) i i = x

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

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

theorem Orthogonalization.MvN.single_mul_single_ne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {i j : Fin n} (h : i ≠ j) (x y : H →L[ℂ] H) : single i x * single j y = 0

theorem Orthogonalization.MvN.single_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (i : Fin n) : single i 0 = 0

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

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

theorem Orthogonalization.MvN.single_inj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {i : Fin n} {x y : H →L[ℂ] H} (h : single i x = single i y) : x = y

theorem Orthogonalization.MvN.isStarProjection_single {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (i : Fin n) {x : H →L[ℂ] H} (hx : IsStarProjection x) : IsStarProjection (single i x)

theorem Orthogonalization.MvN.isStarProjection_of_single {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {i : Fin n} {x : H →L[ℂ] H} (h : IsStarProjection (single i x)) : IsStarProjection x

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

theorem Orthogonalization.MvN.sum_single {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (q : Fin n → H →L[ℂ] H) : ∑ i : Fin n, single i (q i) = FinDim.blockProj q

theorem Orthogonalization.MvN.single_mul_blockProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (i : Fin n) (x : H →L[ℂ] H) (q : Fin n → H →L[ℂ] H) : single i x * FinDim.blockProj q = single i (x * q i)

theorem Orthogonalization.MvN.blockProj_mul_single {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (q : Fin n → H →L[ℂ] H) (i : Fin n) (x : H →L[ℂ] H) : FinDim.blockProj q * single i x = single i (q i * x)

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

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

theorem Orthogonalization.MvN.entry_single_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (i : Fin n) (y : H →L[ℂ] H) (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (j k : Fin n) : entry (single i y * X) j k = if j = i then y * entry X i k else 0

theorem Orthogonalization.MvN.entry_mul_single {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i : Fin n) (y : H →L[ℂ] H) (j k : Fin n) : entry (X * single i y) j k = if k = i then entry X j i * y else 0

theorem Orthogonalization.MvN.entry_eq_conj_of_conj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {i : Fin n} {z : H →L[ℂ] H} {X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)} (h : single i z * X * single i z = X) : z * entry X i i * z = entry X i i

An operator with X = (e_{ii} ⊗ z) X (e_{ii} ⊗ z) has its (i, i) entry in the corner z (·) z.

theorem Orthogonalization.MvN.eq_single_of_conj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {i : Fin n} {z : H →L[ℂ] H} {X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)} (h : single i z * X * single i z = X) : X = single i (entry X i i)

An operator with X = (e_{ii} ⊗ z) X (e_{ii} ⊗ z) is supported in the (i, i) block.

Column operators ∑ᵢ e_{ik} ⊗ X i

noncomputable def Orthogonalization.MvN.col {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (k : Fin n) (X : Fin n → H →L[ℂ] H) : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)

The column operator col k X = ∑ᵢ e_{ik} ⊗ X i on H^n (blocks X i in column k).

Equations

• Orthogonalization.MvN.col k X = Orthogonalization.FinDim.blockMap X ∘SL Orthogonalization.FinDim.proj k

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

theorem Orthogonalization.MvN.col_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) : col k X ∈ matrixAlgebra M n

theorem Orthogonalization.MvN.star_col_mul_col {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (k : Fin n) (X Y : Fin n → H →L[ℂ] H) : star (col k X) * col k Y = single k (∑ i : Fin n, star (X i) * Y i)

(col k X)* (col k Y) = e_{kk} ⊗ ∑ᵢ (X i)* (Y i).

theorem Orthogonalization.MvN.col_mul_single {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (k : Fin n) (X : Fin n → H →L[ℂ] H) (y : H →L[ℂ] H) : col k X * single k y = col k fun (i : Fin n) => X i * y

theorem Orthogonalization.MvN.blockProj_mul_col {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (q : Fin n → H →L[ℂ] H) (k : Fin n) (X : Fin n → H →L[ℂ] H) : FinDim.blockProj q * col k X = col k fun (i : Fin n) => q i * X i

theorem Orthogonalization.MvN.star_col_mul_single_mul_col {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (k : Fin n) (X : Fin n → H →L[ℂ] H) (i : Fin n) (y : H →L[ℂ] H) : star (col k X) * single i y * col k X = single k (star (X i) * y * X i)

(col k X)* (e_{ii} ⊗ y) (col k X) = e_{kk} ⊗ (X i)* y (X i).

Square roots

theorem Orthogonalization.MvN.sqrt_blockProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {q : Fin n → H →L[ℂ] H} (h : ∀ (i : Fin n), 0 ≤ q i) : CFC.sqrt (FinDim.blockProj q) = FinDim.blockProj fun (i : Fin n) => CFC.sqrt (q i)

The square root of a block-diagonal positive operator is block-diagonal.

theorem Orthogonalization.MvN.sqrt_single {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (i : Fin n) {y : H →L[ℂ] H} (hy : 0 ≤ y) : CFC.sqrt (single i y) = single i (CFC.sqrt y)

theorem Orthogonalization.MvN.sqrt_apply_eq_zero_of {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {a : H →L[ℂ] H} (ha : 0 ≤ a) {ξ : H} (h : a ξ = 0) : (CFC.sqrt a) ξ = 0

√a ξ = 0 whenever a ξ = 0 (a ≥ 0): ‖√a ξ‖² = ⟪ξ, a ξ⟫.

theorem Orthogonalization.MvN.sqrt_mul_proj_eq_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {a p : H →L[ℂ] H} (ha : 0 ≤ a) (h : a * p = a) : CFC.sqrt a * p = CFC.sqrt a

If a p = a with a ≥ 0 then √a p = √a (the kernels of a and √a agree).

Right and left supports

theorem Orthogonalization.MvN.isStarProjection_rightSupport {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) : IsStarProjection (rightSupport x)

theorem Orthogonalization.MvN.isStarProjection_leftSupport {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) : IsStarProjection (leftSupport x)

theorem Orthogonalization.MvN.mul_rightSupport {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) : x * rightSupport x = x

x (rightSupport x) = x: 1 − rightSupport x projects onto the (closed) kernel of x.

theorem Orthogonalization.MvN.rightSupport_mul_eq_self_of {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x Q : H →L[ℂ] H} (h : x * Q = x) : rightSupport x * Q = rightSupport x

The right support of x lies below every projection Q with x Q = x (Q need not even be a projection: x (1 − Q) = 0 puts range (1 − Q) inside ker x).

theorem Orthogonalization.MvN.leftSupport_mul_eq_self_of {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x P : H →L[ℂ] H} (hP : IsStarProjection P) (h : P * x = x) : leftSupport x * P = leftSupport x

The left support of x lies below every projection P with P x = x: the closure of range x is inside the closed range of P.

theorem Orthogonalization.MvN.sqrt_star_mul_self_mul_rightSupport {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) : CFC.sqrt (star x * x) * rightSupport x = CFC.sqrt (star x * x)

√(x* x) (rightSupport x) = √(x* x).

The diagonal trace on a corner

theorem Orthogonalization.MvN.sum_entry_star_mul_self_eq_of_corner {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {n : ℕ} {p : H →L[ℂ] H} (hp : IsStarProjection p) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) (hE : ∀ x ∈ M, p * x * p = x → ∀ y ∈ M, p * y * p = y → 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) (hVp : ∀ (i j : Fin n), p * entry V i j * p = entry V i j) : ∑ 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 E tracial on the corner p M p and V with entries in p M p.