Dyadic pairs: finite pairs with no abelian projections

The orthonormalization step of the C6b port (povm_orthogonalization_finitePair, in MIPRE/Background/Orthonormalization/FinitePairOrtho.lean) applies in the first algebra of a finite pair whose operators contain no nonzero abelian projection: no projection r with (r x r)(r y r) = (r y r)(r x r) for all of the algebra's x, y. This file gives a class of finite pairs in which that holds on both sides, by a trace estimate and no comparison theory (reports/c6b-paper-proofs.md, §3, Theorems K, K′ and Cl).

• Cauchy–Schwarz in a commutative corner (mul_star_le_mul_of_commute): for operators x, y with α = x⋆x, β = y⋆y, γ = x⋆y, if α commutes with β and β with γ, then γ γ⋆ ≤ α β. The proof writes (β + ε)(α (β + ε) − γ γ⋆) as z⋆z + ε γ γ⋆ and lets ε → 0.
• The trace estimate (VecTrace.card_mul_re_tr_le_one, Theorem K1): in a set s of operators closed under products and adjoints, with a faithful tracial vector functional tr and unital ι × ι matrix units f, an abelian projection p has |ι| · Re tr p ≤ 1. With wᵢ = f_{i₀ i} p and X = ∑ᵢ wᵢ wᵢ⋆: tr X = tr p, Re tr X² ≤ Re tr p by the corner Cauchy–Schwarz applied to the commuting p fᵢⱼ p, and X lives under f_{i₀ i₀}, whose trace is 1/|ι|; positivity of tr (X − c f_{i₀ i₀})² at c = |ι| tr p gives the bound.
• No abelian projections (VecTrace.eq_zero_of_dyadicUnits, Theorem K2): with units of every size 2ⁿ, an abelian projection has trace 0, so vanishes, the trace being faithful.
• Finite pairs (IsFinitePair.eq_zero_of_abelianA, .eq_zero_of_abelianB, Theorem K′): in a finite pair whose first algebra has unital dyadic matrix units, the first player's operators contain no nonzero abelian projection, in the form of the hypothesis hII of povm_orthogonalization_finitePair; and likewise for the second.
• The class (BipartiteModel.IsDyadicPair): finite pairs whose two algebras have unital dyadic matrix units (MIPRE/Foundations/MatUnits.lean). It is closed under the exchange of the players (IsDyadicPair.swap) and ancilla extensions (IsDyadicPair.expand), the two model operations at the boundary of LIDT.Simul.SoundFin.
• Values (CommutingFinitePairApprox): below ω_co(G), and above 0, lies the value of a projective strategy for G in a dyadic pair on a Hilbert space of Type. It is the statement LIDT.Simul.SoundFin is used through; the proof, on the Background side (MIPRE.Repetition.commutingFinitePairApprox), amplifies the finite pairs of Lin's tracial density by the twisted Pauli algebra.

Cauchy–Schwarz in a commutative corner

theorem MIPRE.mul_star_le_mul_of_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x y α β γ : H →L[ℂ] H} (hα : star x * x = α) (hβ : star y * y = β) (hγ : star x * y = γ) (h1 : Commute α β) (h2 : Commute β γ) : γ * star γ ≤ α * β

Cauchy–Schwarz in a commutative corner (thm:no-abelian-dyadic, the tool of its proof): for operators x, y with α = x⋆x, β = y⋆y and γ = x⋆y, if α commutes with β and β with γ, then γ γ⋆ ≤ α β.

The trace functional of a vector trace

noncomputable def MIPRE.VecTrace.tr {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) : (H →L[ℂ] H) →ₗ[ℂ] ℂ

The functional of a vector trace, on all operators: tr T = ∑ₖ ⟪gₖ, T gₖ⟫, a linear functional.

Equations

• τ.tr = { toFun := fun (T : H →L[ℂ] H) => ∑ k : Fin τ.n, inner ℂ (τ.g k) (T (τ.g k)), map_add' := ⋯, map_smul' := ⋯ }

theorem MIPRE.VecTrace.tr_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) : τ.tr 1 = 1

The functional is normalized.

theorem MIPRE.VecTrace.tr_mul_comm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) {T S : H →L[ℂ] H} (hT : T ∈ s) (hS : S ∈ s) : τ.tr (T * S) = τ.tr (S * T)

The functional is tracial on the set.

theorem MIPRE.VecTrace.re_tr_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) {T : H →L[ℂ] H} (hT : 0 ≤ T) : 0 ≤ (τ.tr T).re

The functional is positive.

theorem MIPRE.VecTrace.re_tr_mono {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) {T S : H →L[ℂ] H} (h : T ≤ S) : (τ.tr T).re ≤ (τ.tr S).re

The real part of the functional is monotone.

theorem MIPRE.VecTrace.tr_star_mul_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) [CompleteSpace H] (T : H →L[ℂ] H) : τ.tr (star T * T) = ↑(∑ k : Fin τ.n, ‖T (τ.g k)‖ ^ 2)

tr (T⋆T) = ∑ₖ ‖T gₖ‖².

The trace estimate, and no abelian projections

theorem MIPRE.VecTrace.card_mul_re_tr_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) (hmul : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s) (hstar : ∀ x ∈ s, star x ∈ s) {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i0 : ι) {f : ι → ι → H →L[ℂ] H} (hf : IsMatUnits f) (hfs : ∀ (i j : ι), f i j ∈ s) {p : H →L[ℂ] H} (hpP : IsStarProjection p) (hps : p ∈ s) (hab : ∀ x ∈ s, ∀ y ∈ s, p * x * p * (p * y * p) = p * y * p * (p * x * p)) : ↑(Fintype.card ι) * (τ.tr p).re ≤ 1

An abelian projection has trace at most 1/|ι| (thm:no-abelian-dyadic, item K1; Theorem K1 of reports/c6b-paper-proofs.md, §3): in a set s of operators closed under products and adjoints, with a faithful tracial vector functional τ and unital ι × ι matrix units in s, a projection p ∈ s with (p x p)(p y p) = (p y p)(p x p) for all x, y ∈ s has |ι| · Re tr p ≤ 1.

theorem MIPRE.VecTrace.eq_zero_of_dyadicUnits {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : Set (H →L[ℂ] H)} (τ : VecTrace s) (hmul : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s) (hstar : ∀ x ∈ s, star x ∈ s) (hunits : ∀ (n : ℕ), ∃ (f : (Fin n → Fin 2) → (Fin n → Fin 2) → H →L[ℂ] H), IsMatUnits f ∧ ∀ (i j : Fin n → Fin 2), f i j ∈ s) {p : H →L[ℂ] H} (hpP : IsStarProjection p) (hps : p ∈ s) (hab : ∀ x ∈ s, ∀ y ∈ s, p * x * p * (p * y * p) = p * y * p * (p * x * p)) : p = 0

No nonzero abelian projection (thm:no-abelian-dyadic, item K2; Theorem K2 of reports/c6b-paper-proofs.md, §3): in a set s of operators closed under products and adjoints, with a faithful tracial vector functional τ and unital matrix units in s of every size 2ⁿ, a projection p ∈ s with (p x p)(p y p) = (p y p)(p x p) for all x, y ∈ s is 0.

Finite pairs with dyadic matrix units

theorem MIPRE.BipartiteModel.mul_mem_opsA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {x y : M.H →L[ℂ] M.H} (hx : x ∈ M.opsA) (hy : y ∈ M.opsA) : x * y ∈ M.opsA

The first player's operators are closed under products.

theorem MIPRE.BipartiteModel.star_mem_opsA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {x : M.H →L[ℂ] M.H} (hx : x ∈ M.opsA) : star x ∈ M.opsA

The first player's operators are closed under adjoints.

theorem MIPRE.BipartiteModel.IsFinitePair.eq_zero_of_abelianA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hU : HasDyadicUnits 𝒜) {r : M.H →L[ℂ] M.H} (hr : r ∈ M.opsA) (hrP : IsStarProjection r) (hab : ∀ x ∈ M.opsA, ∀ y ∈ M.opsA, r * x * r * (r * y * r) = r * y * r * (r * x * r)) : r = 0

No nonzero abelian projection among the first player's operators (thm:no-abelian-dyadic, item K′; Theorem K′ of reports/c6b-paper-proofs.md, §3): in a finite pair whose first algebra has unital dyadic matrix units, a projection r of the first player's operators with (r x r)(r y r) = (r y r)(r x r) for all of them is 0. The hypothesis hII of povm_orthogonalization_finitePair is fun r hr => hM.eq_zero_of_abelianA hU hr.

theorem MIPRE.BipartiteModel.IsFinitePair.eq_zero_of_abelianB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hU : HasDyadicUnits ℬ) {r : M.H →L[ℂ] M.H} (hr : r ∈ M.opsB) (hrP : IsStarProjection r) (hab : ∀ x ∈ M.opsB, ∀ y ∈ M.opsB, r * x * r * (r * y * r) = r * y * r * (r * x * r)) : r = 0

No nonzero abelian projection among the second player's operators (thm:no-abelian-dyadic, item K′): the same for the second algebra, through the exchange of the players.

structure MIPRE.BipartiteModel.IsDyadicPair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : Prop

A dyadic pair (def:dyadic-pair): a finite pair whose two algebras have unital matrix units of every size 2ⁿ. Neither player's operators contain a nonzero abelian projection (IsDyadicPair.eq_zero_of_abelianA, .eq_zero_of_abelianB).

• isFinitePair : M.IsFinitePair

  The model is a finite pair.

• unitsA : HasDyadicUnits 𝒜

  The first player's algebra has unital dyadic matrix units.

• unitsB : HasDyadicUnits ℬ

  The second player's algebra has unital dyadic matrix units.

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

A dyadic pair with the players exchanged is a dyadic pair (lem:dyadic-pair-closure).

theorem MIPRE.BipartiteModel.IsDyadicPair.expand {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : M.IsDyadicPair) {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Nonempty α] [Nonempty β] (e : α × β → ℂ) : (M.expand e).IsDyadicPair

An ancilla extension of a dyadic pair is a dyadic pair (lem:dyadic-pair-closure), for nonempty registers: the units of the extension's algebras are the scalar diagonals of those of the model.

theorem MIPRE.BipartiteModel.IsDyadicPair.eq_zero_of_abelianA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : M.IsDyadicPair) {r : M.H →L[ℂ] M.H} (hr : r ∈ M.opsA) (hrP : IsStarProjection r) (hab : ∀ x ∈ M.opsA, ∀ y ∈ M.opsA, r * x * r * (r * y * r) = r * y * r * (r * x * r)) : r = 0

No nonzero abelian projection among the first player's operators of a dyadic pair (lem:dyadic-pair-closure), in the form of the hypothesis hII of povm_orthogonalization_finitePair.

theorem MIPRE.BipartiteModel.IsDyadicPair.eq_zero_of_abelianB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : M.IsDyadicPair) {r : M.H →L[ℂ] M.H} (hr : r ∈ M.opsB) (hrP : IsStarProjection r) (hab : ∀ x ∈ M.opsB, ∀ y ∈ M.opsB, r * x * r * (r * y * r) = r * y * r * (r * x * r)) : r = 0

No nonzero abelian projection among the second player's operators of a dyadic pair (lem:dyadic-pair-closure).

Values in dyadic pairs

def MIPRE.CommutingFinitePairApprox : Prop

ω_co is approached by projective strategies in dyadic pairs (def:dyadic-pair; proved as lem:co-value-finite-pair): below ω_co(G), and above 0, lies the value of a projective strategy for G in a dyadic pair (BipartiteModel.IsDyadicPair) on a Hilbert space of Type. Proved from Lin's tracial density and an amplification by the twisted Pauli algebra (MIPRE.Repetition.commutingFinitePairApprox).

Equations

• One or more equations did not get rendered due to their size.