The bipartite model: a state and two commuting representations

The stage analyses of compression are bipartite and vector-state: a unit vector, the first player's operators and the second player's, the two families commuting, and never a trace (reports/co-generalization-audit.md). Their common generalization, the model of Phase 1 of planning/mipco-track.md, is a bipartite model (BipartiteModel): a state model (MIPRE/Foundations/StateModel.lean: a Hilbert space H, a state ψ, and a ⋆-algebra 𝒞 represented on H) with two ⋆-algebras 𝒜 (the first player's) and ℬ (the second player's) mapped into 𝒞 by ⋆-homomorphisms πA and πB whose images commute. That ψ is a unit vector is a hypothesis of the results that need it, as in the matrix calculus.

The players' operators are elements of 𝒜 and of ℬ. So a product, a sum or an adjoint of one player's operators is again one of that player's, and it commutes with the other player's for free: this is what the matrix analyses get from writing the two players' operators on the two factors of a tensor product, and what lets them be read in this model unchanged. There are two instances.

• The tensor-product model BipartiteModel.tensor ψ: 𝒞 = M_{dA × dB}(ℂ), 𝒜 = M_{dA}(ℂ), ℬ = M_{dB}(ℂ), πA = aOp and πB = bOp, the Kronecker embeddings of MIPRE/Foundations/OpBound.lean, and 𝒞 acting on EuclideanSpace ℂ (dA × dB). Its products and sums are literally the matrix ones, so the matrix calculus is the model's calculus with nothing to translate (snorm_tensor, qform_tensor, bnd_tensor).
• The commuting-operator model CommutingOperatorStrategy.toModel S: 𝒞 = B(H), 𝒜 the commutant of the second player's operators and ℬ the commutant of 𝒜. They commute by construction, contain the two players' operators (E_mem_aliceAlg, F_mem_bobAlg), and are ordered, since a commutant contains the square roots of its positive elements (starOrderedRing_centralizer): positivity in them is positivity in B(H), which is what the measurements of the analyses need.

structure MIPRE.BipartiteModel (𝒞 : Type v) (𝒜 : Type w) (ℬ : Type x) [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] extends MIPRE.StateModel 𝒞 : Type (max (max (max (u + 1) v) w) x)

A bipartite model: a state model, and two ⋆-algebras, the first player's and the second player's, mapped into its algebra by ⋆-homomorphisms with commuting images.

• H : Type u
• normedAddCommGroup : NormedAddCommGroup self.H
• innerProductSpace : InnerProductSpace ℂ self.H
• completeSpace : CompleteSpace self.H
• ψ : self.H
• π : 𝒞 →⋆ₐ[ℂ] self.H →L[ℂ] self.H
• πA : 𝒜 →⋆ₐ[ℂ] 𝒞

  The first player's algebra.

• πB : ℬ →⋆ₐ[ℂ] 𝒞

  The second player's algebra.

• commute (a : 𝒜) (b : ℬ) : Commute (self.πA a) (self.πB b)

  The two players' operators commute.

def MIPRE.BipartiteModel.swap {𝒞 : Type v} {𝒜 : Type w} {ℬ : Type x} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : BipartiteModel 𝒞 ℬ 𝒜

The model with the two players exchanged.

Equations

• M.swap = { toStateModel := M.toStateModel, πA := M.πB, πB := M.πA, commute := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.swap_toStateModel {𝒞 : Type v} {𝒜 : Type w} {ℬ : Type x} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : M.swap.toStateModel = M.toStateModel

@[simp]

theorem MIPRE.BipartiteModel.swap_πA {𝒞 : Type v} {𝒜 : Type w} {ℬ : Type x} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : M.swap.πA = M.πB

@[simp]

theorem MIPRE.BipartiteModel.swap_πB {𝒞 : Type v} {𝒜 : Type w} {ℬ : Type x} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : M.swap.πB = M.πA

@[simp]

theorem MIPRE.BipartiteModel.swap_swap {𝒞 : Type v} {𝒜 : Type w} {ℬ : Type x} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : M.swap.swap = M

theorem MIPRE.BipartiteModel.bnd_πA_of_isStarProjection {𝒞 : Type v} {𝒜 : Type w} {ℬ : Type x} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {p : 𝒜} (hp : IsStarProjection p) : M.Bnd (M.πA p) 1

A self-adjoint idempotent of the first player's algebra is bounded by one.

theorem MIPRE.BipartiteModel.bnd_πB_of_isStarProjection {𝒞 : Type v} {𝒜 : Type w} {ℬ : Type x} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {q : ℬ} (hq : IsStarProjection q) : M.Bnd (M.πB q) 1

A self-adjoint idempotent of the second player's algebra is bounded by one.

The tensor-product model

noncomputable def MIPRE.BipartiteModel.aOpStarAlgHom {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] : Matrix dA dA ℂ →⋆ₐ[ℂ] Matrix (dA × dB) (dA × dB) ℂ

X ↦ X ⊗ 1, the first factor's matrices acting on the product, as a ⋆-algebra homomorphism.

Equations

• MIPRE.BipartiteModel.aOpStarAlgHom = { toFun := MIPRE.aOp, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

noncomputable def MIPRE.BipartiteModel.bOpStarAlgHom {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] : Matrix dB dB ℂ →⋆ₐ[ℂ] Matrix (dA × dB) (dA × dB) ℂ

Y ↦ 1 ⊗ Y, the second factor's matrices acting on the product, as a ⋆-algebra homomorphism.

Equations

• MIPRE.BipartiteModel.bOpStarAlgHom = { toFun := MIPRE.bOp, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.aOpStarAlgHom_apply {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (X : Matrix dA dA ℂ) : aOpStarAlgHom X = aOp X

@[simp]

theorem MIPRE.BipartiteModel.bOpStarAlgHom_apply {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (Y : Matrix dB dB ℂ) : bOpStarAlgHom Y = bOp Y

noncomputable def MIPRE.BipartiteModel.tensor {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) : BipartiteModel (Matrix (dA × dB) (dA × dB) ℂ) (Matrix dA dA ℂ) (Matrix dB dB ℂ)

The tensor-product model of a vector ψ on ℂ^{dA × dB}: the first player's matrices act as X ⊗ 1, the second player's as 1 ⊗ Y, and the product's matrices act on EuclideanSpace ℂ (dA × dB).

Equations

• MIPRE.BipartiteModel.tensor ψ = { toStateModel := MIPRE.StateModel.mat ψ, πA := MIPRE.BipartiteModel.aOpStarAlgHom, πB := MIPRE.BipartiteModel.bOpStarAlgHom, commute := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.tensor_toStateModel {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) : (tensor ψ).toStateModel = StateModel.mat ψ

@[simp]

theorem MIPRE.BipartiteModel.tensor_πA {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (X : Matrix dA dA ℂ) : (tensor ψ).πA X = aOp X

@[simp]

theorem MIPRE.BipartiteModel.tensor_πB {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (Y : Matrix dB dB ℂ) : (tensor ψ).πB Y = bOp Y

theorem MIPRE.BipartiteModel.snorm_tensor {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (T : Matrix (dA × dB) (dA × dB) ℂ) : (tensor ψ).snorm T = snorm ψ T

The matrix state norm is the state norm of the tensor-product model, by definition.

theorem MIPRE.BipartiteModel.qform_tensor {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (T : Matrix (dA × dB) (dA × dB) ℂ) : (tensor ψ).qform T = qform ψ T

The matrix quadratic form is the quadratic form of the tensor-product model.

theorem MIPRE.BipartiteModel.bnd_tensor {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) {T : Matrix (dA × dB) (dA × dB) ℂ} {K : ℝ} : (tensor ψ).Bnd T K ↔ Bnd T K

The matrix bound is the bound of the tensor-product model.

Positive contractions

The facts about an operator between 0 and 1 that the measurements of the analyses need. Each is a product of two commuting positive operators, which is where the functional calculus of B(H) enters; the players' algebras need not have one.

theorem MIPRE.Op.mul_self_le_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : H →L[ℂ] H} (h0 : 0 ≤ P) (h1 : P ≤ 1) : P * P ≤ P

P² ≤ P for 0 ≤ P ≤ 1: P (1 - P) is a product of commuting positive operators.

theorem MIPRE.Op.bnd_one_of_nonneg_of_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : H →L[ℂ] H} (h0 : 0 ≤ P) (h1 : P ≤ 1) : Bnd P 1

An operator between 0 and 1 is a contraction.

theorem MIPRE.Op.bnd_one_of_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P Q : H →L[ℂ] H} (hP0 : 0 ≤ P) (hP1 : P ≤ 1) (hQ0 : 0 ≤ Q) (hQ1 : Q ≤ 1) : Bnd (P - Q) 1

The difference of two operators between 0 and 1 is a contraction: 1 - (P - Q) and 1 + (P - Q) are commuting positive operators, and their product is 1 - (P - Q)².

The commutant of a set of operators is ordered

theorem MIPRE.starOrderedRing_centralizer {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : Set (H →L[ℂ] H)) : StarOrderedRing ↥(StarSubalgebra.centralizer ℂ s)

A commutant of operators is a star-ordered ring with the order of B(H): a positive element is the square of its square root, which commutes with everything the element commutes with and so lies in the commutant.

The commuting-operator model

noncomputable def MIPRE.CommutingOperatorStrategy.aliceAlg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : StarSubalgebra ℂ (S.H →L[ℂ] S.H)

The first player's algebra: the commutant of the second player's operators.

Equations

• S.aliceAlg = StarSubalgebra.centralizer ℂ (Set.range fun (p : Y × B) => S.F p.1 p.2)

noncomputable def MIPRE.CommutingOperatorStrategy.bobAlg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : StarSubalgebra ℂ (S.H →L[ℂ] S.H)

The second player's algebra: the commutant of the first player's algebra.

Equations

• S.bobAlg = StarSubalgebra.centralizer ℂ ↑S.aliceAlg

instance MIPRE.CommutingOperatorStrategy.instStarOrderedRingSubtypeContinuousLinearMapComplexIdHMemStarSubalgebraAliceAlg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : StarOrderedRing ↥S.aliceAlg

instance MIPRE.CommutingOperatorStrategy.instStarOrderedRingSubtypeContinuousLinearMapComplexIdHMemStarSubalgebraBobAlg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : StarOrderedRing ↥S.bobAlg

theorem MIPRE.CommutingOperatorStrategy.E_mem_aliceAlg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (a : A) : S.E x a ∈ S.aliceAlg

theorem MIPRE.CommutingOperatorStrategy.F_mem_bobAlg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (y : Y) (b : B) : S.F y b ∈ S.bobAlg

theorem MIPRE.CommutingOperatorStrategy.commute_of_mem {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) {a b : S.H →L[ℂ] S.H} (ha : a ∈ S.aliceAlg) (hb : b ∈ S.bobAlg) : Commute a b

The two players' algebras commute, by construction.

noncomputable def MIPRE.CommutingOperatorStrategy.toModel {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : BipartiteModel (S.H →L[ℂ] S.H) ↥S.aliceAlg ↥S.bobAlg

The commuting-operator model of a strategy: its space and state, with B(H) as the algebra, the commutant of the second player's operators as the first player's algebra, and the commutant of that as the second player's.

Equations

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

theorem MIPRE.CommutingOperatorStrategy.toModel_ψ_norm {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : ‖S.toModel.ψ‖ = 1

@[simp]

theorem MIPRE.CommutingOperatorStrategy.toModel_πA {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (a : ↥S.aliceAlg) : S.toModel.πA a = ↑a

@[simp]

theorem MIPRE.CommutingOperatorStrategy.toModel_πB {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (b : ↥S.bobAlg) : S.toModel.πB b = ↑b