Projective commuting-operator strategies, by a commutation-preserving dilation

The first item of Phase 1 of planning/mipco-track.md: the commuting-operator value ω_co is attained on projective commuting-operator strategies (CommutingOperatorStrategy.IsProjective), those whose measurement operators are all orthogonal projections. This is the model the stage analyses are to be generalized over (reports/co-generalization-audit.md §4, mechanism 2): they use projectivity, while ω_co is defined with positive operator valued measures.

The dilation. For a strategy S and a question x of the first player, put s a := √E^x_a (the continuous functional calculus square root, which commutes with everything commuting with E^x_a, in particular with every F^y_b). The Naimark matrix of s at a fixed answer a₀ is a partial isometry, and its Halmos unitary U on S.H ⊗ ℂ^(A ⊕ A) turns the diagonal projections onto the coordinates into a projection-valued measure P_a = U* Q_a U (MIPRE/Foundations/HalmosDilation.lean). The dilated strategy S.dilateLeft x a₀ lives on S.H ⊗ ℂ^(A ⊕ A) with the state ψ ⊗ e_{inl a₀}; the first player measures P_a at x and E^{x'}_a ⊗ 1 at the other questions, the second measures F^y_b ⊗ 1. Then:

• P_a compresses to E^x_a at ψ ⊗ e_{inl a₀}, as an operator identity, and the embedding intertwines each c ⊗ 1 with c, so the correlation is unchanged (correlation_dilateLeft);
• P_a commutes with every F^y_b ⊗ 1, since every entry of U does, so the dilation is again a commuting-operator strategy;
• the amplification c ↦ c ⊗ 1 is a ⋆-homomorphism, so every question that was projective stays projective, and x becomes projective.

The second player's questions are dilated the same way with the players exchanged (CommutingOperatorStrategy.swap, dilateRight). One question at a time, first all of the first player's and then all of the second's, gives a projective strategy with the same correlation (exists_isProjective_correlation_eq), hence ω_co is the supremum over projective strategies (commutingOperatorValue_eq_iSup_isProjective), in the form a soundness proof consumes (exists_isProjective_lt_value). The tensor-product strategies are projective commuting-operator strategies (TensorProductStrategy.isProjective_toCommuting), so the projective model contains both the tensor-product and the commuting-operator values.

No von Neumann algebra theory is used, and no comparison of projections: the defect projections of the Naimark partial isometry are never compared, which is what the finite-dimensional dilation of MIPRE/Foundations/Dilation.lean does by counting dimensions.

def MIPRE.CommutingOperatorStrategy.IsProjective {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : Prop

A commuting-operator strategy is projective when every measurement operator is idempotent; being positive, the operators are then orthogonal projections.

Equations

• S.IsProjective = ((∀ (x : X) (a : A), IsIdempotentElem (S.E x a)) ∧ ∀ (y : Y) (b : B), IsIdempotentElem (S.F y b))

def MIPRE.CommutingOperatorStrategy.swap {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : CommutingOperatorStrategy Y X B A

The strategy with the two players exchanged.

Equations

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

@[simp]

theorem MIPRE.CommutingOperatorStrategy.swap_E {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : S.swap.E = S.F

@[simp]

theorem MIPRE.CommutingOperatorStrategy.swap_F {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : S.swap.F = S.E

theorem MIPRE.CommutingOperatorStrategy.correlation_swap {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (y : Y) (x : X) (b : B) (a : A) : S.swap.correlation y x b a = S.correlation x y a b

Exchanging the players transposes the correlation, since the two players' operators commute.

theorem MIPRE.CommutingOperatorStrategy.nonempty_left {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) : Nonempty A

A question of the first player has an answer: its measurement sums to one on a nonzero space.

theorem MIPRE.CommutingOperatorStrategy.nonempty_right {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (y : Y) : Nonempty B

A question of the second player has an answer.

The square roots of the first player's effects

noncomputable def MIPRE.CommutingOperatorStrategy.sqrtE {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (a : A) : S.H →L[ℂ] S.H

The square root of the first player's effect E^x_a.

Equations

• S.sqrtE x a = CFC.sqrt (S.E x a)

theorem MIPRE.CommutingOperatorStrategy.star_sqrtE {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (a : A) : star (S.sqrtE x a) = S.sqrtE x a

theorem MIPRE.CommutingOperatorStrategy.sqrtE_mul_self {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (a : A) : S.sqrtE x a * S.sqrtE x a = S.E x a

theorem MIPRE.CommutingOperatorStrategy.sum_sqrtE_mul_self {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) : ∑ a : A, S.sqrtE x a * S.sqrtE x a = 1

theorem MIPRE.CommutingOperatorStrategy.commute_F_sqrtE {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : Commute (S.F y b) (S.sqrtE x a)

The square roots commute with the second player's operators.

The dilation of one question of the first player

noncomputable def MIPRE.CommutingOperatorStrategy.dilProj {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) (x : X) (a₀ a : A) : Matrix (A ⊕ A) (A ⊕ A) (S.H →L[ℂ] S.H)

The dilated projection-valued measure of the question x, as a matrix of operators on S.H ⊗ ℂ^(A ⊕ A): the Halmos dilation of the Naimark matrix of a ↦ √E^x_a at a₀.

Equations

• S.dilProj x a₀ a = MIPRE.Halmos.proj (MIPRE.Halmos.naimark (S.sqrtE x) a₀) a

theorem MIPRE.CommutingOperatorStrategy.isStarProjection_dilProj {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) (x : X) (a₀ a : A) : IsStarProjection (S.dilProj x a₀ a)

theorem MIPRE.CommutingOperatorStrategy.sum_dilProj {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) (x : X) (a₀ : A) : ∑ a : A, S.dilProj x a₀ a = 1

theorem MIPRE.CommutingOperatorStrategy.dilProj_inl_inl {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) (x : X) (a₀ a : A) : S.dilProj x a₀ a (Sum.inl a₀) (Sum.inl a₀) = S.E x a

theorem MIPRE.CommutingOperatorStrategy.commute_diagonal_F_dilProj {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) (x : X) (y : Y) (a₀ a : A) (b : B) : Commute (Matrix.diagonal fun (x : A ⊕ A) => S.F y b) (S.dilProj x a₀ a)

noncomputable def MIPRE.CommutingOperatorStrategy.dilateLeft {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) (x : X) (a₀ : A) : CommutingOperatorStrategy X Y A B

The commutation-preserving dilation of the first player's question x, on S.H ⊗ ℂ^(A ⊕ A) with the state ψ ⊗ e_{inl a₀}: the first player measures the dilated projection-valued measure at x and E^{x'}_a ⊗ 1 elsewhere, the second measures F^y_b ⊗ 1.

Equations

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

theorem MIPRE.CommutingOperatorStrategy.dilateLeft_E_self {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) (x : X) (a₀ a : A) : (S.dilateLeft x a₀).E x a = OperatorMatrix.toCLM (S.dilProj x a₀ a)

theorem MIPRE.CommutingOperatorStrategy.dilateLeft_E_of_ne {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) {x x' : X} (h : x' ≠ x) (a₀ a : A) : (S.dilateLeft x a₀).E x' a = OperatorMatrix.amplify (S.E x' a)

theorem MIPRE.CommutingOperatorStrategy.dilateLeft_F {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) (x : X) (a₀ : A) (y : Y) (b : B) : (S.dilateLeft x a₀).F y b = OperatorMatrix.amplify (S.F y b)

theorem MIPRE.CommutingOperatorStrategy.correlation_dilateLeft {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) (x : X) (a₀ : A) : (S.dilateLeft x a₀).correlation = S.correlation

The dilation preserves the correlation.

theorem MIPRE.CommutingOperatorStrategy.isIdempotentElem_dilateLeft_E_self {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) (x : X) (a₀ a : A) : IsIdempotentElem ((S.dilateLeft x a₀).E x a)

theorem MIPRE.CommutingOperatorStrategy.isIdempotentElem_dilateLeft_E_of_ne {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) {x x' : X} (h : x' ≠ x) (a₀ : A) {a : A} (hE : IsIdempotentElem (S.E x' a)) : IsIdempotentElem ((S.dilateLeft x a₀).E x' a)

theorem MIPRE.CommutingOperatorStrategy.isIdempotentElem_dilateLeft_F {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq A] (S : CommutingOperatorStrategy X Y A B) (x : X) (a₀ : A) {y : Y} {b : B} (hF : IsIdempotentElem (S.F y b)) : IsIdempotentElem ((S.dilateLeft x a₀).F y b)

The dilation of one question of the second player

noncomputable def MIPRE.CommutingOperatorStrategy.dilateRight {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq Y] [DecidableEq B] (S : CommutingOperatorStrategy X Y A B) (y : Y) (b₀ : B) : CommutingOperatorStrategy X Y A B

The commutation-preserving dilation of the second player's question y: the first player's dilation, with the players exchanged.

Equations

• S.dilateRight y b₀ = (S.swap.dilateLeft y b₀).swap

theorem MIPRE.CommutingOperatorStrategy.correlation_dilateRight {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq Y] [DecidableEq B] (S : CommutingOperatorStrategy X Y A B) (y : Y) (b₀ : B) : (S.dilateRight y b₀).correlation = S.correlation

theorem MIPRE.CommutingOperatorStrategy.isIdempotentElem_dilateRight_F_self {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq Y] [DecidableEq B] (S : CommutingOperatorStrategy X Y A B) (y : Y) (b₀ b : B) : IsIdempotentElem ((S.dilateRight y b₀).F y b)

theorem MIPRE.CommutingOperatorStrategy.isIdempotentElem_dilateRight_F_of_ne {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq Y] [DecidableEq B] (S : CommutingOperatorStrategy X Y A B) {y y' : Y} (h : y' ≠ y) (b₀ : B) {b : B} (hF : IsIdempotentElem (S.F y' b)) : IsIdempotentElem ((S.dilateRight y b₀).F y' b)

theorem MIPRE.CommutingOperatorStrategy.isIdempotentElem_dilateRight_E {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq Y] [DecidableEq B] (S : CommutingOperatorStrategy X Y A B) (y : Y) (b₀ : B) {x : X} {a : A} (hE : IsIdempotentElem (S.E x a)) : IsIdempotentElem ((S.dilateRight y b₀).E x a)

Every strategy has a projective one with the same correlation

theorem MIPRE.CommutingOperatorStrategy.exists_isProjective_correlation_eq {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : ∃ (T : CommutingOperatorStrategy X Y A B), T.IsProjective ∧ T.correlation = S.correlation

Every commuting-operator strategy has a projective one with the same correlation: the first player's questions are dilated one at a time, then the second player's.

theorem MIPRE.CommutingOperatorStrategy.exists_isProjective_value_eq {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (G : Game X Y A B) : ∃ (T : CommutingOperatorStrategy X Y A B), T.IsProjective ∧ value G T = value G S

Every commuting-operator strategy has a projective one with the same value.

theorem MIPRE.commutingOperatorValue_eq_iSup_isProjective {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : commutingOperatorValue G = ⨆ (T : { T : CommutingOperatorStrategy X Y A B // T.IsProjective }), CommutingOperatorStrategy.value G ↑T

The commuting-operator value is attained on projective strategies: it is the supremum of the values of the projective commuting-operator strategies.

theorem MIPRE.exists_isProjective_lt_value {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {t : ℝ} (ht : 0 ≤ t) (h : t < commutingOperatorValue G) : ∃ (T : CommutingOperatorStrategy X Y A B), T.IsProjective ∧ t < CommutingOperatorStrategy.value G T

A strategy witnessing a lower bound on ω_co can be taken projective: the form in which a soundness proof consumes the dilation.

theorem MIPRE.TensorProductStrategy.isProjective_toCommuting {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) : S.toCommuting.IsProjective

Tensor-product strategies are projective commuting-operator strategies, so the projective model contains the tensor-product model.