Transport of commuting-operator strategies

The commuting-operator counterparts of the transport lemmas of GameTransport.lean and GameDouble.lean, for the bipartite commuting-operator value ω_co (MIPRE.commutingOperatorValue), in which the MIP^co = coRE track reads the halting reduction (planning/mipco-track.md, Phase 0):

• Relabeling. commutingOperatorValue_eq_of_equiv: games related by equivalences of their four alphabets, with matching distribution and decision predicate, have the same commuting-operator value. Strategies are transported by CommutingOperatorStrategy.relabel.
• Monotonicity. commutingOperatorValue_mono: accepting more answer tuples, on the same alphabets and distribution, can only raise the value. A commuting-operator strategy does not mention the game it is played in, so the same strategy is played.
• Answer extension. commutingOperatorValue_extendAnswers: enlarging the answer alphabets by answers that are always rejected does not change the value. From the small game to the large one a strategy extends by the zero operator on the new answers (CommutingOperatorStrategy.extendAnswers); from the large game to the small one the new answers are merged into an old one (CommutingOperatorStrategy.mergeAnswers). For POVMs the merge is a sum of positive operators and needs none of the orthogonality that ProjectiveMeasurement.merge does.
• Doubling. commutingOperatorValue_doubled: the doubled game (MIPRE.Game.doubled) has the commuting-operator value of the game it doubles, by the same two relabelings as quantumValue_doubled and the same computation Game.sum_doubled.

Relabeling

def MIPRE.CommutingOperatorStrategy.relabel {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (eX : X' → X) (eY : Y' → Y) (eA : A' ≃ A) (eB : B' ≃ B) : CommutingOperatorStrategy X' Y' A' B'

Play S through relabelings of the questions (any maps) and of the answers (equivalences). The Hilbert space and the state are those of S.

Equations

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

@[simp]

theorem MIPRE.CommutingOperatorStrategy.relabel_correlation {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (eX : X' → X) (eY : Y' → Y) (eA : A' ≃ A) (eB : B' ≃ B) (x' : X') (y' : Y') (a' : A') (b' : B') : (S.relabel eX eY eA eB).correlation x' y' a' b' = S.correlation (eX x') (eY y') (eA a') (eB b')

theorem MIPRE.CommutingOperatorStrategy.value_relabel {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (G : Game X Y A B) (G' : Game X' Y' A' B') (eX : X' ≃ X) (eY : Y' ≃ Y) (eA : A' ≃ A) (eB : B' ≃ B) (hμ : ∀ (x' : X') (y' : Y'), G'.μ x' y' = G.μ (eX x') (eY y')) (hD : ∀ (x' : X') (y' : Y') (a' : A') (b' : B'), G'.D x' y' a' b' = G.D (eX x') (eY y') (eA a') (eB b')) : value G' (S.relabel (⇑eX) (⇑eY) eA eB) = value G S

Relabeling along equivalences with matching distribution and decision predicate preserves the value.

theorem MIPRE.CommutingOperatorStrategy.value_le_of_accepts_imp {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) (G G' : Game X Y A B) (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G.D x y a b = true → G'.D x y a b = true) : value G S ≤ value G' S

Accepting more answer tuples raises the value of a strategy.

Answer extension and merging

noncomputable def MIPRE.CommutingOperatorStrategy.extendAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (ιA : A ↪ A') (ιB : B ↪ B') : CommutingOperatorStrategy X Y A' B'

Extend the answer alphabets along embeddings, with the zero operator on the new answers.

Equations

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

@[simp]

theorem MIPRE.CommutingOperatorStrategy.extendAnswers_E_apply {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (ιA : A ↪ A') (ιB : B ↪ B') (x : X) (a : A) : (S.extendAnswers ιA ιB).E x (ιA a) = S.E x a

theorem MIPRE.CommutingOperatorStrategy.extendAnswers_E_of_not_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] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (ιA : A ↪ A') (ιB : B ↪ B') (x : X) {a' : A'} (h : ¬∃ (a : A), ιA a = a') : (S.extendAnswers ιA ιB).E x a' = 0

@[simp]

theorem MIPRE.CommutingOperatorStrategy.extendAnswers_F_apply {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (ιA : A ↪ A') (ιB : B ↪ B') (y : Y) (b : B) : (S.extendAnswers ιA ιB).F y (ιB b) = S.F y b

theorem MIPRE.CommutingOperatorStrategy.extendAnswers_F_of_not_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] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (ιA : A ↪ A') (ιB : B ↪ B') (y : Y) {b' : B'} (h : ¬∃ (b : B), ιB b = b') : (S.extendAnswers ιA ιB).F y b' = 0

theorem MIPRE.CommutingOperatorStrategy.correlation_extendAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (ιA : A ↪ A') (ιB : B ↪ B') (x : X) (y : Y) (a : A) (b : B) : (S.extendAnswers ιA ιB).correlation x y (ιA a) (ιB b) = S.correlation x y a b

On the old answers the extended strategy has the old correlation.

theorem MIPRE.CommutingOperatorStrategy.correlation_extendAnswers_of_not_mem_left {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (ιA : A ↪ A') (ιB : B ↪ B') (x : X) (y : Y) {a' : A'} (b' : B') (h : ¬∃ (a : A), ιA a = a') : (S.extendAnswers ιA ιB).correlation x y a' b' = 0

Off the range of ιA the extended strategy has correlation 0.

theorem MIPRE.CommutingOperatorStrategy.correlation_extendAnswers_of_not_mem_right {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (ιA : A ↪ A') (ιB : B ↪ B') (x : X) (y : Y) (a' : A') {b' : B'} (h : ¬∃ (b : B), ιB b = b') : (S.extendAnswers ιA ιB).correlation x y a' b' = 0

Off the range of ιB the extended strategy has correlation 0.

theorem MIPRE.CommutingOperatorStrategy.value_extendAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] (S : CommutingOperatorStrategy X Y A B) (ιA : A ↪ A') (ιB : B ↪ B') (G : Game X Y A B) (G' : Game X Y A' B') (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G'.D x y (ιA a) (ιB b) = G.D x y a b) : value G' (S.extendAnswers ιA ιB) = value G S

Zero extension preserves the value, whatever the decision predicate does on the new answers: their terms vanish.

noncomputable def MIPRE.CommutingOperatorStrategy.mergeAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] (S' : CommutingOperatorStrategy X Y A' B') (rA : A' → A) (rB : B' → B) : CommutingOperatorStrategy X Y A B

Merge the answers along maps back to smaller alphabets: the effect of a is the sum of the effects of the answers a' with r a' = a. For POVMs this needs no orthogonality: a sum of positive operators is positive, the fibers partition the alphabet, and sums of operators that commute with one another commute.

Equations

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

@[simp]

theorem MIPRE.CommutingOperatorStrategy.mergeAnswers_E {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] (S' : CommutingOperatorStrategy X Y A' B') (rA : A' → A) (rB : B' → B) (x : X) (a : A) : (S'.mergeAnswers rA rB).E x a = ∑ a' : A' with rA a' = a, S'.E x a'

@[simp]

theorem MIPRE.CommutingOperatorStrategy.mergeAnswers_F {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] (S' : CommutingOperatorStrategy X Y A' B') (rA : A' → A) (rB : B' → B) (y : Y) (b : B) : (S'.mergeAnswers rA rB).F y b = ∑ b' : B' with rB b' = b, S'.F y b'

theorem MIPRE.CommutingOperatorStrategy.correlation_mergeAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] (S' : CommutingOperatorStrategy X Y A' B') (rA : A' → A) (rB : B' → B) (x : X) (y : Y) (a : A) (b : B) : (S'.mergeAnswers rA rB).correlation x y a b = ∑ a' : A' with rA a' = a, ∑ b' : B' with rB b' = b, S'.correlation x y a' b'

The Born-rule weight of a merged answer pair is the sum of the weights over the fibers.

theorem MIPRE.CommutingOperatorStrategy.value_le_mergeAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] (S' : CommutingOperatorStrategy X Y A' B') (rA : A' → A) (rB : B' → B) (G' : Game X Y A' B') (G : Game X Y A B) (hμ : ∀ (x : X) (y : Y), G.μ x y = G'.μ x y) (hD : ∀ (x : X) (y : Y) (a' : A') (b' : B'), G'.D x y a' b' = true → G.D x y (rA a') (rB b') = true) : value G' S' ≤ value G (S'.mergeAnswers rA rB)

Merging can only raise the value, when every accepted tuple of the large game is accepted after merging.

The commuting-operator value under transport

theorem MIPRE.commutingOperatorValue_eq_of_equiv {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] (G : Game X Y A B) (G' : Game X' Y' A' B') (eX : X' ≃ X) (eY : Y' ≃ Y) (eA : A' ≃ A) (eB : B' ≃ B) (hμ : ∀ (x' : X') (y' : Y'), G'.μ x' y' = G.μ (eX x') (eY y')) (hD : ∀ (x' : X') (y' : Y') (a' : A') (b' : B'), G'.D x' y' a' b' = G.D (eX x') (eY y') (eA a') (eB b')) : commutingOperatorValue G' = commutingOperatorValue G

Games related by equivalences of their alphabets, with matching distribution and decision predicate, have the same commuting-operator value.

theorem MIPRE.commutingOperatorValue_mono {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G G' : Game X Y A B) (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G.D x y a b = true → G'.D x y a b = true) : commutingOperatorValue G ≤ commutingOperatorValue G'

Accepting more answer tuples, on the same alphabets and distribution, raises the commuting-operator value.

theorem MIPRE.commutingOperatorValue_eq_zero_of_reject {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G.D x y a b = false) : commutingOperatorValue G = 0

A game whose decision predicate rejects everything has commuting-operator value 0.

theorem MIPRE.commutingOperatorValue_extendAnswers {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_5} {B' : Type u_6} [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] (G : Game X Y A B) (G' : Game X Y A' B') (ιA : A ↪ A') (ιB : B ↪ B') (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G'.D x y (ιA a) (ιB b) = G.D x y a b) (hD' : ∀ (x : X) (y : Y) (a' : A') (b' : B'), G'.D x y a' b' = true → (∃ (a : A), ιA a = a') ∧ ∃ (b : B), ιB b = b') : commutingOperatorValue G' = commutingOperatorValue G

Enlarging the answer alphabets by always-rejected answers does not change the commuting-operator value. G' on A' × B' accepts (ιA a, ιB b) exactly when G accepts (a, b), and accepts nothing off the ranges of the embeddings.

The doubled game

def MIPRE.CommutingOperatorStrategy.undouble {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] (S : CommutingOperatorStrategy (Bool × X) (Bool × X) A A) : CommutingOperatorStrategy X X A A

A strategy for the doubled game, read on the original: the first player keeps the effects at (false, ·), the second those at (true, ·).

Equations

• S.undouble = S.relabel (fun (x : X) => (false, x)) (fun (y : X) => (true, y)) (Equiv.refl A) (Equiv.refl A)

def MIPRE.CommutingOperatorStrategy.double {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] (S : CommutingOperatorStrategy X X A A) : CommutingOperatorStrategy (Bool × X) (Bool × X) A A

A strategy for the original game, read on the doubled one: both players ignore the tag.

Equations

• S.double = S.relabel (fun (p : Bool × X) => p.2) (fun (q : Bool × X) => q.2) (Equiv.refl A) (Equiv.refl A)

theorem MIPRE.CommutingOperatorStrategy.value_undouble {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : Game X X A A) (S : CommutingOperatorStrategy (Bool × X) (Bool × X) A A) : value G S.undouble = value G.doubled.toGame S

theorem MIPRE.CommutingOperatorStrategy.value_double {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : Game X X A A) (S : CommutingOperatorStrategy X X A A) : value G.doubled.toGame S.double = value G S

theorem MIPRE.commutingOperatorValue_doubled {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : Game X X A A) : commutingOperatorValue G.doubled.toGame = commutingOperatorValue G

The doubling preserves the commuting-operator value. Each direction is one strategy transported and one comparison with the supremum.