The actual hiding normalizer is the propagated question prefix #
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the normalizer is an element of
the second player's algebra, and the estimate is in the second player's state norm of the model.
noncomputable def
MIPRE.Introspection.TypedEstimates.hidingNormalizer
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{A : Type u_6}
[Field F]
[Fintype F]
[Fintype ι]
[DecidableEq ι]
[Fintype PauliAnswer]
[Fintype A]
{ℓ : ℕ}
{R : Type u_7}
[Ring R]
[StarRing R]
[PartialOrder R]
[StarOrderedRing R]
(P : CL.CLFun F ι ℓ)
(k : ℕ)
(N : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R)
(y : Option (ι → F))
:
R
The actual conditional marginal, including its malformed-answer outcome.
Equations
- MIPRE.Introspection.TypedEstimates.hidingNormalizer P k N y = ∑ z : Option ((ι → F) × (ι → F) × (ι → F)), (MIPRE.POVMIn.map (MIPRE.Introspection.TypedEstimates.hidingNextLater P k) N).op (y, z)
Instances For
theorem
MIPRE.Introspection.TypedEstimates.hidingNormalizer_eq_reportedPrefix
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{A : Type u_6}
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype PauliAnswer]
[Fintype A]
{ℓ : ℕ}
{R : Type u_7}
[Ring R]
[StarRing R]
[PartialOrder R]
[StarOrderedRing R]
(P : CL.CLFun F ι ℓ)
(k : ℕ)
(j : Fin ℓ)
(N : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R)
(y : Option (ι → F))
:
Summing the tested later outcomes gives exactly its reported prefix PVM; the dummy outcome is included on both sides of the identity.
theorem
MIPRE.Introspection.TypedEstimates.hidingNormalizer_estimate
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype PauliAnswer]
[Fintype A]
{ℓ : ℕ}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype κ]
[DecidableEq κ]
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
(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)
(Q : Option (ι → F) → ℬ)
(hintro :
∑ y : Option (ι → F),
Ψ.snorm
(Ψ.πB
((POVMIn.map (reportedPrefix (L w) (↑k + 1) AuxType.introspect) (MB (QuestionType.introspect w, 0))).op y - Q y)) ^ 2 ≤ δ)
:
The actual prefix chain discharges the later hiding normalizer estimate from the single Introspect-prefix estimate. No assumption about later hiding operators or a supplied conditional marginal is needed.