Merging strategy answers separately at each question

Deterministic answer decoding can depend on the question. Merging the fibers of these maps preserves projectivity, register dimensions and the shared state. Acceptance implication gives monotonicity of the resulting value.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): for a projective strategy of a model (BipartiteModel.ProjStrat) the merge is the coarse-graining of each measurement along its own question's decoder, fun x => (S'.PA x).map (rA x), which is the adapter ProjStrat.adapt along the identity of the questions (BipartiteModel.ProjStrat.mergeAnswersByQuestion). The merged strategy is a strategy of the same model, so there is no state or register dimension to preserve, and a question whose decoder is the identity keeps its measurement (mergeByQuestionPAEq, mergeByQuestionPBEq, equalities of POVMs). The value bound is BipartiteModel.povmValue_le_postprocess; the tensor-product statements are its instances in the tensor-product model of a strategy (TensorProductStrategy.value_mergeAnswersByQuestion, through ProjectiveMeasurement.mergeByQuestion_toIn).

def MIPRE.ProjectiveMeasurement.mergeByQuestion {X : Type u_1} {A : Type u_2} {A' : Type u_3} {H : Type u_4} [Fintype A] [Fintype A'] [DecidableEq A] [Fintype H] [DecidableEq H] (P : ProjectiveMeasurement X A' (Matrix H H ℂ)) (r : X → A' → A) : ProjectiveMeasurement X A (Matrix H H ℂ)

Merge each question's effects along its own answer map.

Equations

• P.mergeByQuestion r = { M := fun (x : X) (a : A) => (P.merge (r x)).M x a, selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.ProjectiveMeasurement.mergeByQuestion_M {X : Type u_1} {A : Type u_2} {A' : Type u_3} {H : Type u_4} [Fintype A] [Fintype A'] [DecidableEq A] [Fintype H] [DecidableEq H] (P : ProjectiveMeasurement X A' (Matrix H H ℂ)) (r : X → A' → A) (x : X) (a : A) : (P.mergeByQuestion r).M x a = ∑ a' : A' with r x a' = a, P.M x a'

A merged effect is the sum over the decoding fiber at that question.

theorem MIPRE.ProjectiveMeasurement.mergeByQuestion_toIn {X : Type u_1} {A : Type u_2} {A' : Type u_3} {H : Type u_4} [Fintype A] [Fintype A'] [DecidableEq A] [Fintype H] [DecidableEq H] (P : ProjectiveMeasurement X A' (Matrix H H ℂ)) (r : X → A' → A) (x : X) : ((P.mergeByQuestion r).toPOVM x).toIn = POVMIn.map (r x) (P.toPOVM x).toIn

The merged measurement is a coarse-graining in the matrix algebra: at each question, the fiber sums of the original POVM along that question's decoder (POVMIn.map).

In a bipartite model

def MIPRE.BipartiteModel.ProjStrat.mergeAnswersByQuestion {𝒞 : 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} {A' : Type u_8} {B' : Type u_9} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] {G' : Game X Y A' B'} (S' : M.ProjStrat G') (G : Game X Y A B) (rA : X → A' → A) (rB : Y → B' → B) : M.ProjStrat G

Decode answers by a question-dependent function: at each question, the measurement of S' with its outcomes merged along that question's decoder. It is the adapter along the identity of the questions, a strategy of the same model.

Equations

• S'.mergeAnswersByQuestion G rA rB = S'.adapt G (fun (x : X) => x) (fun (y : Y) => y) rA rB

@[simp]

theorem MIPRE.BipartiteModel.ProjStrat.mergeAnswersByQuestion_PA {𝒞 : 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} {A' : Type u_8} {B' : Type u_9} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] {G' : Game X Y A' B'} (S' : M.ProjStrat G') (G : Game X Y A B) (rA : X → A' → A) (rB : Y → B' → B) (x : X) : (S'.mergeAnswersByQuestion G rA rB).PA x = POVMIn.map (rA x) (S'.PA x)

A merged first-player measurement is the coarse-graining along the question's decoder.

@[simp]

theorem MIPRE.BipartiteModel.ProjStrat.mergeAnswersByQuestion_PB {𝒞 : 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} {A' : Type u_8} {B' : Type u_9} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] {G' : Game X Y A' B'} (S' : M.ProjStrat G') (G : Game X Y A B) (rA : X → A' → A) (rB : Y → B' → B) (y : Y) : (S'.mergeAnswersByQuestion G rA rB).PB y = POVMIn.map (rB y) (S'.PB y)

A merged second-player measurement is the coarse-graining along the question's decoder.

theorem MIPRE.BipartiteModel.ProjStrat.value_le_mergeAnswersByQuestion {𝒞 : 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} {A' : Type u_8} {B' : Type u_9} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] {G' : Game X Y A' B'} (S' : M.ProjStrat G') (G : Game X Y A B) (rA : X → A' → A) (rB : Y → 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' b' = true → G.D x y (rA x a') (rB y b') = true) : S'.value ≤ (S'.mergeAnswersByQuestion G rA rB).value

Acceptance-preserving answer decoding can only increase the value, on the same question law (BipartiteModel.povmValue_le_postprocess).

theorem MIPRE.BipartiteModel.ProjStrat.mergeByQuestionPAEq {𝒞 : 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] [DecidableEq A] [DecidableEq B] {G' : Game X Y A B} (S' : M.ProjStrat G') (G : Game X Y A B) (rA : X → A → A) (rB : Y → B → B) (x : X) (hr : ∀ (a : A), rA x a = a) : (S'.mergeAnswersByQuestion G rA rB).PA x = S'.PA x

Identity decoding at a first-player question keeps its measurement, under a same-alphabet answer merge.

theorem MIPRE.BipartiteModel.ProjStrat.mergeByQuestionPBEq {𝒞 : 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] [DecidableEq A] [DecidableEq B] {G' : Game X Y A B} (S' : M.ProjStrat G') (G : Game X Y A B) (rA : X → A → A) (rB : Y → B → B) (y : Y) (hr : ∀ (b : B), rB y b = b) : (S'.mergeAnswersByQuestion G rA rB).PB y = S'.PB y

Identity decoding at a second-player question keeps its measurement, under a same-alphabet answer merge.

theorem MIPRE.BipartiteModel.ProjStrat.mergeByQuestionPAEq_op {𝒞 : 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] [DecidableEq A] [DecidableEq B] {G' : Game X Y A B} (S' : M.ProjStrat G') (G : Game X Y A B) (rA : X → A → A) (rB : Y → B → B) (x : X) (a : A) (hr : ∀ (a : A), rA x a = a) : ((S'.mergeAnswersByQuestion G rA rB).PA x).op a = (S'.PA x).op a

Identity decoding at a first-player question keeps each of its effects.

theorem MIPRE.BipartiteModel.ProjStrat.mergeByQuestionPBEq_op {𝒞 : 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] [DecidableEq A] [DecidableEq B] {G' : Game X Y A B} (S' : M.ProjStrat G') (G : Game X Y A B) (rA : X → A → A) (rB : Y → B → B) (y : Y) (b : B) (hr : ∀ (b : B), rB y b = b) : ((S'.mergeAnswersByQuestion G rA rB).PB y).op b = (S'.PB y).op b

Identity decoding at a second-player question keeps each of its effects.

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

Decode answers by a question-dependent function, preserving registers and state.

Equations

• S'.mergeAnswersByQuestion G rA rB = { dA := S'.dA, dB := S'.dB, ψ := S'.ψ, ψ_unit := ⋯, PA := S'.PA.mergeByQuestion rA, PB := S'.PB.mergeByQuestion rB }

theorem MIPRE.TensorProductStrategy.value_mergeAnswersByQuestion {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {A' : Type u_5} {B' : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] {G' : Game X Y A' B'} (S' : TensorProductStrategy G') (G : Game X Y A B) (rA : X → A' → A) (rB : Y → B' → B) : (S'.mergeAnswersByQuestion G rA rB).value = (S'.toModel.mergeAnswersByQuestion G rA rB).value

The merged strategy is the model's merged strategy: its value is that of the projective strategy of S' in its tensor-product model (toModel), merged question by question.

theorem MIPRE.SyncStrategy.value_le_copy {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (G' : SynchronousGame X A) (hμ : ∀ (x y : X), G'.μ x y = G.μ x y) (hD : ∀ (x y : X) (a b : A), G.D x y a b = true → G'.D x y a b = true) : S.value ≤ (S.copy G').value

Relaxing a predicate with the same question law can only increase a copied synchronous strategy's value.

theorem MIPRE.SyncStrategy.copy_value_eq_one {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (G' : SynchronousGame X A) (hμ : ∀ (x y : X), G'.μ x y = G.μ x y) (hD : ∀ (x y : X) (a b : A), G.D x y a b = true → G'.D x y a b = true) (hS : S.value = 1) : (S.copy G').value = 1

Copying to a relaxed game preserves perfect success.

@[simp]

theorem MIPRE.SyncStrategy.copy_d {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (G' : SynchronousGame X A) : (S.copy G').d = S.d

Copying a synchronous strategy keeps its dimension.