Strategies in a bipartite model, read in ω_co

The analyses of the stages are written once, for POVM families in a bipartite model (MIPRE/Foundations/BipartiteModel.lean). This file is how such an analysis becomes a statement about the commuting-operator value ω_co, in both directions:

• from the model to ω_co: a POVM strategy in a bipartite model on a Hilbert space is a commuting-operator strategy with the same value (BipartiteModel.toCommuting), so its value is at most ω_co (BipartiteModel.povmValue_le_commutingOperatorValue);
• from ω_co to the model: ω_co is approached by strategies whose measurements are projective in the players' algebras of their own model (exists_isPVMIn_lt_povmValue), by the commutation-preserving dilation of Phase 1(a) (exists_isProjective_lt_value) and the orthogonality of projections summing to one in a C⋆-algebra (IsPVMIn.of_isStarProjection).

So a model-level theorem — projective families of value at least 1 - ε give families in the same model of value at least 1 - f(ε) — bounds ω_co of the second game below by 1 - f(ε) as soon as ω_co of the first exceeds 1 - ε.

Projective measurements from projections

theorem MIPRE.IsPVMIn.of_map {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Fintype Λ] {P : Λ → R} {S : Type u_3} {F : Type u_4} [Ring S] [StarRing S] [FunLike F R S] [RingHomClass F R S] [StarHomClass F R S] {f : F} (hf : Function.Injective ⇑f) (h : IsPVMIn fun (a : Λ) => f (P a)) : IsPVMIn P

An injective unital ⋆-ring homomorphism reflects projective measurements.

theorem MIPRE.IsPVMIn.of_isStarProjection {R : Type u_1} {Λ : Type u_2} [Ring R] [StarRing R] [Fintype Λ] {P : Λ → R} [PartialOrder R] [StarOrderedRing R] (hR : ∀ (x : R), star x * x = 0 → x = 0) (hP : ∀ (a : Λ), IsStarProjection (P a)) (hsum : ∑ a : Λ, P a = 1) : IsPVMIn P

Projections summing to one are mutually orthogonal, in a star-ordered ring in which x⋆ x = 0 forces x = 0 — a C⋆-algebra, for instance. Conjugating ∑_c P_c = 1 by P_a makes the compressions P_a P_c P_a = (P_c P_a)⋆ (P_c P_a), c ≠ a, nonnegative elements summing to zero.

A strategy in a model is a commuting-operator strategy

noncomputable def MIPRE.BipartiteModel.toCommuting {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (hψ : ‖M.ψ‖ = 1) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) : CommutingOperatorStrategy X Y A B

A POVM strategy in a bipartite model is a commuting-operator strategy: the represented operators of the two families, on the model's space and state.

Equations

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

theorem MIPRE.BipartiteModel.correlation_toCommuting {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (hψ : ‖M.ψ‖ = 1) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) (x : X) (y : Y) (a : A) (b : B) : (M.toCommuting hψ MA MB).correlation x y a b = M.bornProb ((MA x).op a) ((MB y).op b)

theorem MIPRE.BipartiteModel.value_toCommuting {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (hψ : ‖M.ψ‖ = 1) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) (G : Game X Y A B) : CommutingOperatorStrategy.value G (M.toCommuting hψ MA MB) = M.povmValue G MA MB

The value of the strategy is its value in the model.

theorem MIPRE.BipartiteModel.povmValue_le_commutingOperatorValue {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (hψ : ‖M.ψ‖ = 1) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) (G : Game X Y A B) : M.povmValue G MA MB ≤ commutingOperatorValue G

The value of a POVM strategy in a bipartite model is at most ω_co.

ω_co is approached by projective strategies in their own model

theorem MIPRE.CommutingOperatorStrategy.isPVMIn_aliceMeas {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {S : CommutingOperatorStrategy X Y A B} (hS : S.IsProjective) (x : X) : IsPVMIn (S.aliceMeas x).op

The first player's measurements of a projective strategy are projective in the first player's algebra of its model.

theorem MIPRE.CommutingOperatorStrategy.isPVMIn_bobMeas {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {S : CommutingOperatorStrategy X Y A B} (hS : S.IsProjective) (y : Y) : IsPVMIn (S.bobMeas y).op

The second player's measurements of a projective strategy are projective in the second player's algebra of its model.

theorem MIPRE.exists_isPVMIn_lt_povmValue {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) : ∃ (S : CommutingOperatorStrategy X Y A B), (∀ (x : X), IsPVMIn (S.aliceMeas x).op) ∧ (∀ (y : Y), IsPVMIn (S.bobMeas y).op) ∧ t < S.toModel.povmValue G S.aliceMeas S.bobMeas

ω_co is approached by strategies projective in their own model: below ω_co, some commuting-operator strategy has model value above the threshold with both players' measurements projective in their algebras.