Documentation

MIPRE.Foundations.Introspection.TypedQuotientReindex

Exact game and PCC transport of quotient answers between coordinate types #

The strategy transport of the soundness direction, reindexedStrategy, is stated in a bipartite model (Phase 4 of planning/mipco-track.md): it relabels the answers of a projective strategy of the quotient game along the answer equivalence (BipartiteModel.ProjStrat.relabel), in the same model, and keeps its value (reindexedStrategy_value). Each of its effects is the original effect at the pulled-back answer (reindexedStrategy_PA_op, reindexedStrategy_PB_op), through POVMIn.map_equiv_op and BipartiteModel.ProjStrat.relabel_PA_op/relabel_PB_op.

Effects of a relabelled strategy #

These belong with POVMIn.map (MIPRE/Foundations/Measurement.lean) and ProjStrat.relabel (MIPRE/Foundations/ModelStrategy.lean), and are here until those modules are next rebuilt.

source
theorem MIPRE.POVMIn.map_equiv_op {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [DecidableEq Y] (e : X ≃ Y) (M : POVMIn X R) (y : Y) :
(map (⇑e) M).op y = M.op (e.symm y)

Relabelling a POVM along an equivalence of its outcomes: the effect of an outcome is the original effect of its preimage.

source
theorem MIPRE.BipartiteModel.ProjStrat.relabel_PA_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} {X' : Type u_8} {Y' : Type u_9} {A' : Type u_10} {B' : Type u_11} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [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') (eX : X' ≃ X) (eY : Y' ≃ Y) (eA : A' ≃ A) (eB : B' ≃ B) (x' : X') (a' : A') :
((S.relabel G' eX eY eA eB).PA x').op a' = (S.PA (eX x')).op (eA a')

A relabelled first-player effect is the original effect at the relabelled question and answer.

source
theorem MIPRE.BipartiteModel.ProjStrat.relabel_PB_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} {X' : Type u_8} {Y' : Type u_9} {A' : Type u_10} {B' : Type u_11} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [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') (eX : X' ≃ X) (eY : Y' ≃ Y) (eA : A' ≃ A) (eB : B' ≃ B) (y' : Y') (b' : B') :
((S.relabel G' eX eY eA eB).PB y').op b' = (S.PB (eY y')).op (eB b')

A relabelled second-player effect is the original effect at the relabelled question and answer.

source
theorem MIPRE.Introspection.AuxiliaryQuotient.prefix_attained_reindex {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} (e : Îč ≃ Îș) (P : CL.CLFun F Îč ℓ) (k : ℕ) (y : Îč → F) :
(∃ (x : Îș → F), (CL.CLFun.truncate k (CL.CLFun.reindex e P)).eval x = (CL.CLFun.reindex e P).outputPrefix k ((CL.reindexEquiv e) y)) ↔ ∃ (x : Îč → F), (CL.CLFun.truncate k P).eval x = P.outputPrefix k y
source
theorem MIPRE.Introspection.AuxiliaryQuotient.prefixGuard_reindex {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} (e : Îč ≃ Îș) (L : Bool → CL.CLFun F Îč ℓ) (t : QuestionType PT ℓ) (a : ParsedAnswer (Îč → F) A PA) :
PrefixGuard.holds (fun (w : Bool) => CL.CLFun.reindex e (L w)) t ((answerEquiv e) a) ↔ PrefixGuard.holds L t a
source
@[reducible, inline]
noncomputable abbrev MIPRE.Introspection.AuxiliaryQuotient.reindexedGame {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) :
Game (CL.Detyping.Question (QuestionType PT ℓ) Q) (CL.Detyping.Question (QuestionType PT ℓ) Q) (ParsedAnswer (Îș → F) A PA) (ParsedAnswer (Îș → F) A PA)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.Introspection.AuxiliaryQuotient.reindexedGame_D {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) (q r : CL.Detyping.Question (QuestionType PT ℓ) Q) (a b : ParsedAnswer (Îč → F) A PA) :
    (reindexedGame e E X Z P L project D DP).D q r ((answerEquiv e) a) ((answerEquiv e) b) = (game E X Z P L project D DP).D q r a b
    source
    @[reducible, inline]
    noncomputable abbrev MIPRE.Introspection.AuxiliaryQuotient.reindexedStrategy {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) {𝒞 : Type u_8} {𝒜 : Type u_9} {ℬ : Type u_10} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Κ : BipartiteModel 𝒞 𝒜 ℬ} (S : Κ.ProjStrat (game E X Z P L project D DP)) :
    Κ.ProjStrat (reindexedGame e E X Z P L project D DP)

    Carry a projective strategy to the concrete coordinate numbering, in the same model: its answers relabelled along the answer equivalence.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.Introspection.AuxiliaryQuotient.reindexedStrategy_value {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) {𝒞 : Type u_8} {𝒜 : Type u_9} {ℬ : Type u_10} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Κ : BipartiteModel 𝒞 𝒜 ℬ} (S : Κ.ProjStrat (game E X Z P L project D DP)) :
      (reindexedStrategy e E X Z P L project D DP S).value = S.value
      source
      theorem MIPRE.Introspection.AuxiliaryQuotient.reindexedStrategy_PA_op {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) {𝒞 : Type u_8} {𝒜 : Type u_9} {ℬ : Type u_10} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Κ : BipartiteModel 𝒞 𝒜 ℬ} (S : Κ.ProjStrat (game E X Z P L project D DP)) (q : CL.Detyping.Question (QuestionType PT ℓ) Q) (a : ParsedAnswer (Îș → F) A PA) :
      ((reindexedStrategy e E X Z P L project D DP S).PA q).op a = (S.PA q).op ((answerEquiv e).symm a)

      A reindexed first-player effect is the original effect at the pulled-back answer.

      source
      theorem MIPRE.Introspection.AuxiliaryQuotient.reindexedStrategy_PB_op {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) {𝒞 : Type u_8} {𝒜 : Type u_9} {ℬ : Type u_10} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Κ : BipartiteModel 𝒞 𝒜 ℬ} (S : Κ.ProjStrat (game E X Z P L project D DP)) (q : CL.Detyping.Question (QuestionType PT ℓ) Q) (a : ParsedAnswer (Îș → F) A PA) :
      ((reindexedStrategy e E X Z P L project D DP S).PB q).op a = (S.PB q).op ((answerEquiv e).symm a)

      A reindexed second-player effect is the original effect at the pulled-back answer.

      source
      @[reducible, inline]
      noncomputable abbrev MIPRE.Introspection.AuxiliaryQuotient.originalPCC {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) [DecidableEq A] [DecidableEq PA] (S : SyncStrategy (reindexedGame e E X Z P L project D DP).doubled) :
      SyncStrategy (game E X Z P L project D DP).doubled
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.Introspection.AuxiliaryQuotient.originalPCC_isPCC {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) [DecidableEq A] [DecidableEq PA] (S : SyncStrategy (reindexedGame e E X Z P L project D DP).doubled) (hS : S.IsPCC) :
        (originalPCC e E X Z P L project D DP S).IsPCC
        source
        theorem MIPRE.Introspection.AuxiliaryQuotient.originalPCC_value {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) [DecidableEq A] [DecidableEq PA] (S : SyncStrategy (reindexedGame e E X Z P L project D DP).doubled) :
        (originalPCC e E X Z P L project D DP S).value = S.value
        source
        @[simp]
        theorem MIPRE.Introspection.AuxiliaryQuotient.originalPCC_dimension {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) [DecidableEq A] [DecidableEq PA] (S : SyncStrategy (reindexedGame e E X Z P L project D DP).doubled) :
        (originalPCC e E X Z P L project D DP S).d = S.d
        source
        theorem MIPRE.Introspection.AuxiliaryQuotient.originalPCC_prefixGuard {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) [DecidableEq A] [DecidableEq PA] (S : SyncStrategy (reindexedGame e E X Z P L project D DP).doubled) (hS : ∀ (q : Bool × CL.Detyping.Question (QuestionType PT ℓ) Q) (a : ParsedAnswer (Îș → F) A PA), S.P.M q a ≠ 0 → PrefixGuard.holds (fun (w : Bool) => CL.CLFun.reindex e (L w)) q.2.1 a) (q : Bool × CL.Detyping.Question (QuestionType PT ℓ) Q) (a : ParsedAnswer (Îč → F) A PA) (ha : (originalPCC e E X Z P L project D DP S).P.M q a ≠ 0) :
        PrefixGuard.holds L q.2.1 a
        source
        @[reducible, inline]
        noncomputable abbrev MIPRE.Introspection.AuxiliaryQuotient.reindexedPCC {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) [DecidableEq A] [DecidableEq PA] (S : SyncStrategy (game E X Z P L project D DP).doubled) :
        SyncStrategy (reindexedGame e E X Z P L project D DP).doubled

        Carry the same honest operators to the concrete coordinate numbering.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem MIPRE.Introspection.AuxiliaryQuotient.reindexedPCC_dimension {F : Type u_1} {Îč : Type u_2} {Îș : Type u_3} {A : Type u_4} {PA : Type u_5} {PT : Type u_6} {Q : Type u_7} [Field F] [Fintype Îč] [DecidableEq Îč] [Fintype Îș] [DecidableEq Îș] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PA] [Fintype PT] [DecidableEq PT] [Fintype Q] [DecidableEq Q] (e : Îč ≃ Îș) (E : PT → PT → Bool) (X Z : PT) (P : PT → CL.CLFun (ZMod 2) Q 3) (L : Bool → CL.CLFun F Îč ℓ) (project : PA → Îč → F) (D : (Îč → F) → (Îč → F) → A → A → Bool) (DP : PT → PT → (Q → ZMod 2) → (Q → ZMod 2) → PA → PA → Bool) [DecidableEq A] [DecidableEq PA] (S : SyncStrategy (game E X Z P L project D DP).doubled) :
          (reindexedPCC e E X Z P L project D DP S).d = S.d