Block-diagonal operators on H ⊕ H

The doubling of a finite pair (reports/c6b-paper-proofs.md, §4; built in MIPRE/Background/LIDT/Co/Doubling/) acts on H ⊕ H = Ampl (Fin 2) H, the first player by the block-diagonal operators u ⊕ v and the second by v ⊕ u, with the state (ψ, ψ)/√2 and the flip (ξ, η) ↦ (η, ξ) exchanging them. This file collects the facts about these operators that name no model:

• Diagonal operators of any finite amplification: toCLM (diagonal d) acts on the i-th copy by d i (toCLM_diagonal_emb_apply), is positive exactly when every d i is (toCLM_diagonal_nonneg_iff), and determines d (toCLM_diagonal_inj); an operator commutes with it exactly when its entries intertwine the d i (commute_toCLM_diagonal_iff).
• The pair embedding diag2 : (H →L[ℂ] H) × (H →L[ℂ] H) →⋆ₐ[ℂ] B(H ⊕ H), (u, v) ↦ u ⊕ v, a unital ⋆-homomorphism (diag2_apply), injective.
• The flip flip2 of the two copies, a self-inverse isometry, which conjugates u ⊕ v to v ⊕ u (flip2_diag2_flip2).
• The half vector halfVec ψ = (ψ, ψ)/√2, fixed by the flip, of the norm of ψ, at which a block-diagonal operator has the average of its blocks' expectations (inner_halfVec_toCLM_diagonal, Lemma 2 of the report).
• Traces (VecTrace.diag2): faithful tracial vector functionals τ on s and σ on t give one on the block-diagonal operators u ⊕ v with u ∈ s, v ∈ t, namely ½ (τ(u) + σ(v)) (VecTrace.tr_diag2), from the vectors (gₖ, 0)/√2 and (0, hₗ)/√2 (Lemma 9).
• No abelian projections (NoAbelianProj, noAbelianProj_diag2Set_iff): the hypothesis hII of the orthonormalization tier povm_orthogonalization_finitePair holds for the block-diagonal operators over s and t exactly when it holds for both (Lemma 11, Theorem F); both algebras of a dyadic pair satisfy it (IsDyadicPair.noAbelianProj_opsA, _opsB).

Diagonal operators of an amplification

theorem MIPRE.OperatorMatrix.toCLM_diagonal_emb_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d : ι → H →L[ℂ] H) (i₀ : ι) (ξ : H) : (toCLM (Matrix.diagonal d)) ((emb i₀) ξ) = (emb i₀) ((d i₀) ξ)

A diagonal matrix acts on the i₀-th copy by its i₀-th entry.

theorem MIPRE.OperatorMatrix.emb_injective {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [DecidableEq ι] (i₀ : ι) : Function.Injective ⇑(emb i₀)

The embedding of a copy is injective.

theorem MIPRE.OperatorMatrix.toCLM_diagonal_nonneg_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d : ι → H →L[ℂ] H) : 0 ≤ toCLM (Matrix.diagonal d) ↔ ∀ (i : ι), 0 ≤ d i

A diagonal operator is positive exactly when its entries are.

theorem MIPRE.OperatorMatrix.toCLM_diagonal_inj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {d d' : ι → H →L[ℂ] H} : toCLM (Matrix.diagonal d) = toCLM (Matrix.diagonal d') ↔ d = d'

A diagonal operator determines its entries.

theorem MIPRE.OperatorMatrix.commute_toCLM_diagonal_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : Ampl ι H →L[ℂ] Ampl ι H) (d : ι → H →L[ℂ] H) : Commute T (toCLM (Matrix.diagonal d)) ↔ ∀ (i j : ι), entries T i j * d j = d i * entries T i j

An operator commutes with a diagonal operator exactly when its entries intertwine the diagonal's: Tᵢⱼ dⱼ = dᵢ Tᵢⱼ.

Two copies: the pair embedding and the flip

noncomputable def MIPRE.OperatorMatrix.pairDiag {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] : R × R →⋆ₐ[ℂ] Matrix (Fin 2) (Fin 2) R

(u, v) ↦ diag(u, v), as a unital ⋆-algebra homomorphism into the 2 × 2 matrices.

Equations

• MIPRE.OperatorMatrix.pairDiag = { toFun := fun (c : R × R) => Matrix.diagonal ![c.1, c.2], map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

noncomputable def MIPRE.OperatorMatrix.diag2 {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : (H →L[ℂ] H) × (H →L[ℂ] H) →⋆ₐ[ℂ] Ampl (Fin 2) H →L[ℂ] Ampl (Fin 2) H

The pair embedding (u, v) ↦ u ⊕ v of two operators on H as a block-diagonal operator on H ⊕ H, a unital ⋆-algebra homomorphism.

Equations

• MIPRE.OperatorMatrix.diag2 = MIPRE.OperatorMatrix.toCLMStarAlgHom.comp MIPRE.OperatorMatrix.pairDiag

theorem MIPRE.OperatorMatrix.diag2_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : (H →L[ℂ] H) × (H →L[ℂ] H)) : diag2 c = toCLM (Matrix.diagonal ![c.1, c.2])

The pair embedding is the operator of the diagonal matrix of the pair.

theorem MIPRE.OperatorMatrix.diag2_injective {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Function.Injective ⇑diag2

The pair embedding is injective.

theorem MIPRE.OperatorMatrix.diag2_nonneg_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : (H →L[ℂ] H) × (H →L[ℂ] H)) : 0 ≤ diag2 c ↔ 0 ≤ c.1 ∧ 0 ≤ c.2

A block-diagonal operator is positive exactly when both blocks are.

noncomputable def MIPRE.OperatorMatrix.flip2 {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Ampl (Fin 2) H ≃ₗᵢ[ℂ] Ampl (Fin 2) H

The flip (ξ, η) ↦ (η, ξ) of the two copies of H.

Equations

• MIPRE.OperatorMatrix.flip2 = LinearIsometryEquiv.piLpCongrLeft 2 ℂ H (Equiv.swap 0 1)

theorem MIPRE.OperatorMatrix.flip2_apply_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (f : Ampl (Fin 2) H) : (flip2 f).ofLp 0 = f.ofLp 1

The first coordinate of the flip is the second coordinate.

theorem MIPRE.OperatorMatrix.flip2_apply_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (f : Ampl (Fin 2) H) : (flip2 f).ofLp 1 = f.ofLp 0

The second coordinate of the flip is the first coordinate.

theorem MIPRE.OperatorMatrix.flip2_flip2 {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (f : Ampl (Fin 2) H) : flip2 (flip2 f) = f

The flip is an involution.

theorem MIPRE.OperatorMatrix.flip2_diag2_flip2 {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : (H →L[ℂ] H) × (H →L[ℂ] H)) (f : Ampl (Fin 2) H) : flip2 ((diag2 c) (flip2 f)) = (diag2 c.swap) f

The flip exchanges the blocks of a block-diagonal operator.

theorem MIPRE.OperatorMatrix.flip2_symm_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (f : Ampl (Fin 2) H) : flip2.symm f = flip2 f

The flip is its own inverse.

theorem MIPRE.OperatorMatrix.conjStarAlgEquiv_flip2_diag2 {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : (H →L[ℂ] H) × (H →L[ℂ] H)) : flip2.conjStarAlgEquiv (diag2 c) = diag2 c.swap

Conjugation by the flip exchanges the blocks: J (u ⊕ v) J = v ⊕ u.

Operators commuting with block-diagonal operators

theorem MIPRE.OperatorMatrix.eq_diag2_of_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : Ampl (Fin 2) H →L[ℂ] Ampl (Fin 2) H} (h : Commute T (diag2 (1, 0))) : T = diag2 (entries T 0 0, entries T 1 1)

An operator commuting with 1 ⊕ 0 is block diagonal, with its diagonal entries as blocks.

theorem MIPRE.OperatorMatrix.commute_entries_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : Ampl (Fin 2) H →L[ℂ] Ampl (Fin 2) H} {u : H →L[ℂ] H} (h : Commute T (diag2 (u, 0))) : Commute (entries T 0 0) u

An operator commuting with u ⊕ 0 has its first diagonal entry commuting with u.

theorem MIPRE.OperatorMatrix.commute_entries_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : Ampl (Fin 2) H →L[ℂ] Ampl (Fin 2) H} {v : H →L[ℂ] H} (h : Commute T (diag2 (0, v))) : Commute (entries T 1 1) v

An operator commuting with 0 ⊕ v has its second diagonal entry commuting with v.

The half vector

theorem MIPRE.OperatorMatrix.ofReal_inv_sqrt_two_mul_self : ↑(√2)⁻¹ * ↑(√2)⁻¹ = 2⁻¹

(√2)⁻¹ * (√2)⁻¹ = ½, as complex numbers.

noncomputable def MIPRE.OperatorMatrix.halfVec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) : Ampl (Fin 2) H

The half vector (ψ, ψ)/√2 of H ⊕ H.

Equations

• MIPRE.OperatorMatrix.halfVec ψ = WithLp.toLp 2 fun (x : Fin 2) => ↑(√2)⁻¹ • ψ

theorem MIPRE.OperatorMatrix.halfVec_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (i : Fin 2) : (halfVec ψ).ofLp i = ↑(√2)⁻¹ • ψ

Both coordinates of the half vector are ψ/√2.

theorem MIPRE.OperatorMatrix.norm_halfVec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) : ‖halfVec ψ‖ = ‖ψ‖

The half vector has the norm of ψ.

theorem MIPRE.OperatorMatrix.flip2_halfVec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) : flip2 (halfVec ψ) = halfVec ψ

The flip fixes the half vector.

theorem MIPRE.OperatorMatrix.inner_halfVec_toCLM_diagonal {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ψ : H) (d : Fin 2 → H →L[ℂ] H) : inner ℂ (halfVec ψ) ((toCLM (Matrix.diagonal d)) (halfVec ψ)) = 2⁻¹ * (inner ℂ ψ ((d 0) ψ) + inner ℂ ψ ((d 1) ψ))

The expectation of a block-diagonal operator at the half vector is the average of its blocks' expectations (Lemma 2 of reports/c6b-paper-proofs.md, §4.3).

theorem MIPRE.OperatorMatrix.inner_halfVec_diag2 {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ψ : H) (c : (H →L[ℂ] H) × (H →L[ℂ] H)) : inner ℂ (halfVec ψ) ((diag2 c) (halfVec ψ)) = 2⁻¹ * (inner ℂ ψ (c.1 ψ) + inner ℂ ψ (c.2 ψ))

The expectation of a block-diagonal operator at the half vector, for the pair embedding.

theorem MIPRE.OperatorMatrix.inner_smul_emb_toCLM_diagonal {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : Fin 2 → H →L[ℂ] H) (i : Fin 2) (ξ : H) : inner ℂ (↑(√2)⁻¹ • (emb i) ξ) ((toCLM (Matrix.diagonal d)) (↑(√2)⁻¹ • (emb i) ξ)) = 2⁻¹ * inner ℂ ξ ((d i) ξ)

A scaled embedded vector, c • emb i ξ with c = (√2)⁻¹, gives half the expectation of the i-th entry of a diagonal operator.

Traces of block-diagonal operators

def MIPRE.VecTrace.diag2Set {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s t : Set (H →L[ℂ] H)) : Set (OperatorMatrix.Ampl (Fin 2) H →L[ℂ] OperatorMatrix.Ampl (Fin 2) H)

The block-diagonal operators u ⊕ v with u ∈ s and v ∈ t.

Equations

• MIPRE.VecTrace.diag2Set s t = Set.image2 (fun (u v : H →L[ℂ] H) => MIPRE.OperatorMatrix.diag2 (u, v)) s t

noncomputable def MIPRE.VecTrace.diag2Vec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {s t : Set (H →L[ℂ] H)} (τ : VecTrace s) (σ : VecTrace t) : Fin τ.n ⊕ Fin σ.n → OperatorMatrix.Ampl (Fin 2) H

The vectors of the doubled trace: (gₖ, 0)/√2 and (0, hₗ)/√2.

Equations

• τ.diag2Vec σ (Sum.inl k) = ↑(√2)⁻¹ • (MIPRE.OperatorMatrix.emb 0) (τ.g k)
• τ.diag2Vec σ (Sum.inr l) = ↑(√2)⁻¹ • (MIPRE.OperatorMatrix.emb 1) (σ.g l)

theorem MIPRE.VecTrace.sum_inner_diag2Vec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s t : Set (H →L[ℂ] H)} (τ : VecTrace s) (σ : VecTrace t) (u v : H →L[ℂ] H) : ∑ m : Fin τ.n ⊕ Fin σ.n, inner ℂ (τ.diag2Vec σ m) ((OperatorMatrix.diag2 (u, v)) (τ.diag2Vec σ m)) = 2⁻¹ * (τ.tr u + σ.tr v)

The doubled functional of a block-diagonal operator is the average of the two functionals.

noncomputable def MIPRE.VecTrace.diag2 {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s t : Set (H →L[ℂ] H)} (τ : VecTrace s) (σ : VecTrace t) : VecTrace (diag2Set s t)

The doubled trace (Lemma 9 of reports/c6b-paper-proofs.md, §4.3): faithful tracial vector functionals τ on s and σ on t give the faithful tracial vector functional u ⊕ v ↦ ½ (τ(u) + σ(v)) on the block-diagonal operators over s and t.

Equations

• τ.diag2 σ = MIPRE.VecTrace.ofFintype (τ.diag2Vec σ) ⋯ ⋯ ⋯

theorem MIPRE.VecTrace.tr_diag2 {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s t : Set (H →L[ℂ] H)} (τ : VecTrace s) (σ : VecTrace t) (u v : H →L[ℂ] H) : (τ.diag2 σ).tr (OperatorMatrix.diag2 (u, v)) = 2⁻¹ * (τ.tr u + σ.tr v)

The functional of the doubled trace is the average of the two functionals: tr(u ⊕ v) = ½ (τ(u) + σ(v)).

Abelian projections

def MIPRE.NoAbelianProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : Set (H →L[ℂ] H)) : Prop

No nonzero abelian projection in a set s of operators: a self-adjoint idempotent r ∈ s whose corner r s r is commutative vanishes. This is the hypothesis hII of the orthonormalization tier povm_orthogonalization_finitePair at s = M.opsA.

Equations

• MIPRE.NoAbelianProj s = ∀ r ∈ s, IsStarProjection r → (∀ x ∈ s, ∀ y ∈ s, r * x * r * (r * y * r) = r * y * r * (r * x * r)) → r = 0

theorem MIPRE.noAbelianProj_diag2Set_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s t : Set (H →L[ℂ] H)} (hs : 0 ∈ s) (ht : 0 ∈ t) : NoAbelianProj (VecTrace.diag2Set s t) ↔ NoAbelianProj s ∧ NoAbelianProj t

No abelian projections in a block-diagonal algebra (Lemma 11, Theorem F of reports/c6b-paper-proofs.md, §4.3): for sets s, t containing 0, the block-diagonal operators over s and t have no nonzero abelian projection exactly when neither s nor t has.

theorem MIPRE.BipartiteModel.IsDyadicPair.noAbelianProj_opsA {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : M.IsDyadicPair) : NoAbelianProj M.opsA

A dyadic pair's first player's operators have no nonzero abelian projection (IsDyadicPair.eq_zero_of_abelianA, in the form NoAbelianProj).

theorem MIPRE.BipartiteModel.IsDyadicPair.noAbelianProj_opsB {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : M.IsDyadicPair) : NoAbelianProj M.opsB

A dyadic pair's second player's operators have no nonzero abelian projection (IsDyadicPair.eq_zero_of_abelianB, in the form NoAbelianProj).