Restricting a game to the support of its question distribution

The counterpart for questions of quantumValue_extendAnswers: a game whose question distribution is supported on the image of embeddings X' ↪ X, Y' ↪ Y has the same quantum value as its restriction to X' × Y', with the distribution and the decision predicate pulled back (quantumValue_restrictQuestions). From the large game to the small one a strategy is played through the embeddings (TensorProductStrategy.relabel, which accepts any question maps); from the small one to the large one it is played through a retraction (Function.invFun), the questions off the image carrying no weight either way.

The consumer is the class verifier of the polynomial-time halting reduction (Halting/Paper/ClassMain.lean): its game has every string of length at most B as a question, while its sampler only ever produces the strings of length s(C) — the compressed sampler's questions at the fixed level — and the two games have the same value.

theorem MIPRE.TensorProductStrategy.value_relabel_of_support {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} [Fintype X'] [Fintype Y'] {G : Game X Y A B} (S : TensorProductStrategy G) (G' : Game X' Y' A B) (eX : X' ↪ X) (eY : Y' ↪ Y) (hμ : ∀ (x' : X') (y' : Y'), G'.μ x' y' = G.μ (eX x') (eY y')) (hμ0 : ∀ (x : X) (y : Y), G.μ x y ≠ 0 → (∃ (x' : X'), eX x' = x) ∧ ∃ (y' : Y'), eY y' = y) (hD : ∀ (x' : X') (y' : Y') (a : A) (b : B), G'.D x' y' a b = G.D (eX x') (eY y') a b) : (S.relabel G' (⇑eX) (⇑eY) (Equiv.refl A) (Equiv.refl B)).value = S.value

Playing a strategy of G on the restriction G' through the embeddings keeps the value, when G's distribution is supported on the image.

theorem MIPRE.TensorProductStrategy.value_relabel_invFun {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} [Fintype X'] [Fintype Y'] [Nonempty X'] [Nonempty Y'] {G' : Game X' Y' A B} (S' : TensorProductStrategy G') (G : Game X Y A B) (eX : X' ↪ X) (eY : Y' ↪ Y) (hμ : ∀ (x' : X') (y' : Y'), G'.μ x' y' = G.μ (eX x') (eY y')) (hμ0 : ∀ (x : X) (y : Y), G.μ x y ≠ 0 → (∃ (x' : X'), eX x' = x) ∧ ∃ (y' : Y'), eY y' = y) (hD : ∀ (x' : X') (y' : Y') (a : A) (b : B), G'.D x' y' a b = G.D (eX x') (eY y') a b) : (S'.relabel G (Function.invFun ⇑eX) (Function.invFun ⇑eY) (Equiv.refl A) (Equiv.refl B)).value = S'.value

Playing a strategy of the restriction G' on G through retractions of the embeddings keeps the value, when G's distribution is supported on the image.

theorem MIPRE.quantumValue_restrictQuestions {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} [Fintype X'] [Fintype Y'] [Nonempty X'] [Nonempty Y'] (G : Game X Y A B) (G' : Game X' Y' A B) (eX : X' ↪ X) (eY : Y' ↪ Y) (hμ : ∀ (x' : X') (y' : Y'), G'.μ x' y' = G.μ (eX x') (eY y')) (hμ0 : ∀ (x : X) (y : Y), G.μ x y ≠ 0 → (∃ (x' : X'), eX x' = x) ∧ ∃ (y' : Y'), eY y' = y) (hD : ∀ (x' : X') (y' : Y') (a : A) (b : B), G'.D x' y' a b = G.D (eX x') (eY y') a b) : quantumValue G' = quantumValue G

Restriction to the support. A game whose question distribution is supported on the image of embeddings X' ↪ X, Y' ↪ Y has the quantum value of its restriction to X' × Y': the game G' with G'.μ x' y' = G.μ (eX x') (eY y') and G'.D x' y' = G.D (eX x') (eY y').

noncomputable def MIPRE.Game.restrict {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} [Fintype X'] [Fintype Y'] (G : Game X Y A B) (eX : X' → X) (eY : Y' → Y) (h : ∑ x' : X', ∑ y' : Y', G.μ (eX x') (eY y') = 1) : Game X' Y' A B

The restriction of a game along question maps whose images carry the whole distribution: the same distribution and decision predicate, pulled back.

Equations

• G.restrict eX eY h = { μ := fun (x' : X') (y' : Y') => G.μ (eX x') (eY y'), μ_nonneg := ⋯, μ_sum_one := h, D := fun (x' : X') (y' : Y') (a : A) (b : B) => G.D (eX x') (eY y') a b }