Documentation

MIPRE.Foundations.Introspection.HidingNormalizer

Normalizer replacement on the parsed adjacent hiding edge #

The test error and conditional relation below are consequences of the actual parsed game's failure. The remaining inputs are the preceding fine rigidity estimate and the later prefix marginal estimate used in the induction.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the strategy is a pair of POVM families in the two players' algebras, the ideal fine and prefix measurements are families in the second player's algebra, and the coarse fine operators are fibSumIn of the first player's measurement.

source
theorem MIPRE.Introspection.TypedEstimates.conditionalCoarseDistance_fibSum {π’ž : Type u_1} {π’œ : Type u_2} {ℬ : Type u_3} [Ring π’ž] [StarRing π’ž] [Algebra β„‚ π’ž] [Ring π’œ] [StarRing π’œ] [Algebra β„‚ π’œ] [Ring ℬ] [StarRing ℬ] [Algebra β„‚ ℬ] [PartialOrder π’œ] [StarOrderedRing π’œ] [PartialOrder ℬ] [StarOrderedRing ℬ] {I : Type u_4} {O : Type u_5} {Y : Type u_6} {Z : Type u_7} [Fintype I] [Fintype O] [DecidableEq O] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (Ξ¨ : BipartiteModel π’ž π’œ ℬ) (M : POVMIn I π’œ) (N : POVMIn O ℬ) (f : Y β†’ I β†’ Z) (g : O β†’ Y Γ— Z) :
conditionalCoarseDistance Ξ¨ M N f g = βˆ‘ p : Y Γ— Z, Ξ¨.snorm (Ξ¨.Ο€B ((POVMIn.map g N).op p) - Ξ¨.Ο€A (fibSumIn M.op (f p.1) p.2) * Ξ¨.Ο€B (βˆ‘ z : Z, (POVMIn.map g N).op (p.1, z))) ^ 2

Express conditional distance in terms of the fine operators, leaving the later measurement's map intact.

source
theorem MIPRE.Introspection.TypedEstimates.hiding_next_condWin_lower {π’ž : Type u_1} {π’œ : Type u_2} {ℬ : Type u_3} [Ring π’ž] [StarRing π’ž] [Algebra β„‚ π’ž] [Ring π’œ] [StarRing π’œ] [Algebra β„‚ π’œ] [Ring ℬ] [StarRing ℬ] [Algebra β„‚ ℬ] [PartialOrder π’œ] [StarOrderedRing π’œ] [PartialOrder ℬ] [StarOrderedRing ℬ] {PauliType : Type u_4} {PauliAnswer : Type u_5} {F : Type u_6} {ΞΉ : Type u_7} {ΞΊ : Type u_8} {A : Type u_9} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Fintype ΞΉ] [DecidableEq ΞΉ] [Fintype ΞΊ] [DecidableEq ΞΊ] [Fintype A] {β„“ : β„•} (E : PauliType β†’ PauliType β†’ Bool) (X Z : PauliType) (P : PauliType β†’ CL.CLFun (ZMod 2) ΞΊ 3) (L : Bool β†’ CL.CLFun F ΞΉ β„“) (projectPauli : PauliAnswer β†’ ΞΉ β†’ F) (D : (ΞΉ β†’ F) β†’ (ΞΉ β†’ F) β†’ A β†’ A β†’ Bool) (DP : PauliType β†’ PauliType β†’ (ΞΊ β†’ ZMod 2) β†’ (ΞΊ β†’ ZMod 2) β†’ PauliAnswer β†’ PauliAnswer β†’ Bool) (Ξ¨ : BipartiteModel π’ž π’œ ℬ) (hΞ¨ : β€–Ξ¨.Οˆβ€– = 1) (MA : CL.Detyping.Question (QuestionType PauliType β„“) ΞΊ β†’ POVMIn (ParsedAnswer (ΞΉ β†’ F) A PauliAnswer) π’œ) (MB : CL.Detyping.Question (QuestionType PauliType β„“) ΞΊ β†’ POVMIn (ParsedAnswer (ΞΉ β†’ F) A PauliAnswer) ℬ) {Ξ΅ : ℝ} (hfail : 1 - Ξ¨.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≀ Ξ΅) (w : Bool) (k j : Fin β„“) (hk : ↑k + 1 = ↑j) :
1 - ↑(TypeGraph.edges E X Z β„“).card * Ξ΅ ≀ Ξ¨.condWin (parsedGame E X Z P L projectPauli D DP) MA MB (QuestionType.hide w k, 0) (QuestionType.hide w j, 0)

Extract the success probability of an actual adjacent hiding edge from the game's uniform ordered-edge distribution.

source
theorem MIPRE.Introspection.TypedEstimates.hiding_next_guarded_estimate {π’ž : Type u_1} {π’œ : Type u_2} {ℬ : Type u_3} [Ring π’ž] [StarRing π’ž] [Algebra β„‚ π’ž] [Ring π’œ] [StarRing π’œ] [Algebra β„‚ π’œ] [Ring ℬ] [StarRing ℬ] [Algebra β„‚ ℬ] [PartialOrder π’œ] [StarOrderedRing π’œ] [PartialOrder ℬ] [StarOrderedRing ℬ] {PauliType : Type u_4} {PauliAnswer : Type u_5} {F : Type u_6} {ΞΉ : Type u_7} {ΞΊ : Type u_8} {A : Type u_9} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Fintype ΞΉ] [DecidableEq ΞΉ] [Fintype ΞΊ] [DecidableEq ΞΊ] [Fintype A] {β„“ : β„•} (E : PauliType β†’ PauliType β†’ Bool) (X Z : PauliType) (P : PauliType β†’ CL.CLFun (ZMod 2) ΞΊ 3) (L : Bool β†’ CL.CLFun F ΞΉ β„“) (projectPauli : PauliAnswer β†’ ΞΉ β†’ F) (D : (ΞΉ β†’ F) β†’ (ΞΉ β†’ F) β†’ A β†’ A β†’ Bool) (DP : PauliType β†’ PauliType β†’ (ΞΊ β†’ ZMod 2) β†’ (ΞΊ β†’ ZMod 2) β†’ PauliAnswer β†’ PauliAnswer β†’ Bool) (Ξ¨ : BipartiteModel π’ž π’œ ℬ) (hΞ¨ : β€–Ξ¨.Οˆβ€– = 1) (MA : CL.Detyping.Question (QuestionType PauliType β„“) ΞΊ β†’ POVMIn (ParsedAnswer (ΞΉ β†’ F) A PauliAnswer) π’œ) (MB : CL.Detyping.Question (QuestionType PauliType β„“) ΞΊ β†’ POVMIn (ParsedAnswer (ΞΉ β†’ F) A PauliAnswer) ℬ) {Ξ΅ : ℝ} (hfail : 1 - Ξ¨.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≀ Ξ΅) (w : Bool) (k j : Fin β„“) (hk : ↑k + 1 = ↑j) (hL : (L w).SupportedOn Finset.univ) (hMB : IsPVMIn (MB (QuestionType.hide w j, 0)).op) :
conditionalCoarseDistance Ξ¨ (POVMIn.map (hidingCoarse (L w) ↑k) (MA (QuestionType.hide w k, 0))) (MB (QuestionType.hide w j, 0)) (hidingNextGuarded (L w) ↑k) (hidingNextLater (L w) ↑k) ≀ 2 * ↑(TypeGraph.edges E X Z β„“).card * Ξ΅

The parsed hiding test supplies conditional consistency after Alice's answer has already been reduced to the preceding hiding label.

source
theorem MIPRE.Introspection.TypedEstimates.hiding_next_normalizer_estimate {π’ž : Type u_1} {π’œ : Type u_2} {ℬ : Type u_3} [Ring π’ž] [StarRing π’ž] [Algebra β„‚ π’ž] [Ring π’œ] [StarRing π’œ] [Algebra β„‚ π’œ] [Ring ℬ] [StarRing ℬ] [Algebra β„‚ ℬ] [PartialOrder π’œ] [StarOrderedRing π’œ] [PartialOrder ℬ] [StarOrderedRing ℬ] {PauliType : Type u_4} {PauliAnswer : Type u_5} {F : Type u_6} {ΞΉ : Type u_7} {ΞΊ : Type u_8} {A : Type u_9} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Fintype ΞΉ] [DecidableEq ΞΉ] [Fintype ΞΊ] [DecidableEq ΞΊ] [Fintype A] {β„“ : β„•} (E : PauliType β†’ PauliType β†’ Bool) (X Z : PauliType) (P : PauliType β†’ CL.CLFun (ZMod 2) ΞΊ 3) (L : Bool β†’ CL.CLFun F ΞΉ β„“) (projectPauli : PauliAnswer β†’ ΞΉ β†’ F) (D : (ΞΉ β†’ F) β†’ (ΞΉ β†’ F) β†’ A β†’ A β†’ Bool) (DP : PauliType β†’ PauliType β†’ (ΞΊ β†’ ZMod 2) β†’ (ΞΊ β†’ ZMod 2) β†’ PauliAnswer β†’ PauliAnswer β†’ Bool) (Ξ¨ : BipartiteModel π’ž π’œ ℬ) (hΞ¨ : β€–Ξ¨.Οˆβ€– = 1) (MA : CL.Detyping.Question (QuestionType PauliType β„“) ΞΊ β†’ POVMIn (ParsedAnswer (ΞΉ β†’ F) A PauliAnswer) π’œ) (MB : CL.Detyping.Question (QuestionType PauliType β„“) ΞΊ β†’ POVMIn (ParsedAnswer (ΞΉ β†’ F) A PauliAnswer) ℬ) {Ξ΅ Ξ· Ξ΅fine : ℝ} (hfail : 1 - Ξ¨.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≀ Ξ΅) (w : Bool) (k j : Fin β„“) (hk : ↑k + 1 = ↑j) (hL : (L w).SupportedOn Finset.univ) (hMA : IsPVMIn (MA (QuestionType.hide w k, 0)).op) (hMB : IsPVMIn (MB (QuestionType.hide w j, 0)).op) (ideal : Option ((ΞΉ β†’ F) Γ— (ΞΉ β†’ F) Γ— (ΞΉ β†’ F)) β†’ ℬ) (Q : Option (ΞΉ β†’ F) β†’ ℬ) (hideal : IsPVMIn ideal) (hprefix : IsPVMIn Q) (hcomm : βˆ€ (y : Option (ΞΉ β†’ F)) (i : Option ((ΞΉ β†’ F) Γ— (ΞΉ β†’ F) Γ— (ΞΉ β†’ F))), Commute (Q y) (ideal i)) (hfine : βˆ‘ i : Option ((ΞΉ β†’ F) Γ— (ΞΉ β†’ F) Γ— (ΞΉ β†’ F)), Ξ¨.xSqNorm ((POVMIn.map (hidingCoarse (L w) ↑k) (MA (QuestionType.hide w k, 0))).op i) (ideal i) ≀ Ξ΅fine) (hnorm : βˆ‘ y : Option (ΞΉ β†’ F), Ξ¨.snorm (Ξ¨.Ο€B (βˆ‘ z : Option ((ΞΉ β†’ F) Γ— (ΞΉ β†’ F) Γ— (ΞΉ β†’ F)), (POVMIn.map (hidingNextLater (L w) ↑k) (MB (QuestionType.hide w j, 0))).op (y, z) - Q y)) ^ 2 ≀ Ξ·) :
βˆ‘ p : Option (ΞΉ β†’ F) Γ— Option ((ΞΉ β†’ F) Γ— (ΞΉ β†’ F) Γ— (ΞΉ β†’ F)), Ξ¨.snorm (Ξ¨.Ο€B ((POVMIn.map (hidingNextLater (L w) ↑k) (MB (QuestionType.hide w j, 0))).op p) - Ξ¨.Ο€B (conditionalIdeal ideal Q (hidingNextGuarded (L w) ↑k) p)) ^ 2 ≀ 6 * ↑(TypeGraph.edges E X Z β„“).card * Ξ΅ + 3 * Ξ· + 3 * Ξ΅fine

Actual hiding normalizer step. Replace the later conditional marginal by a commuting ideal prefix at error 6 |E| Ξ΅ + 3 Ξ· + 3 Ξ΅fine. The keyed map acts on the preceding fine hiding label, and every parsed answer is included.