The local honest hiding step

This identifies the actual stopping Hide measurement with its local dual-X measurement and untouched X tail in the coordinate split used by the next adaptive step.

def MIPRE.Introspection.Honest.coarseOp {I : Type u_1} {A : Type u_3} {B : Type u_4} [Fintype A] [DecidableEq B] (f : A → B) (P : A → Matrix I I ℂ) (b : B) : Matrix I I ℂ

Equations

• MIPRE.Introspection.Honest.coarseOp f P b = ∑ a : A with f a = b, P a

theorem MIPRE.Introspection.Honest.coarseOp_comp {I : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Fintype I] [DecidableEq I] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] (f : A → B) (g : B → C) (P : A → Matrix I I ℂ) (c : C) : coarseOp g (coarseOp f P) c = coarseOp (g ∘ f) P c

theorem MIPRE.Introspection.Honest.coarseOp_first {I : Type u_1} {J : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] (f : A → C) (P : A → Matrix I I ℂ) (Q : B → Matrix J J ℂ) (cb : C × B) : coarseOp (fun (ab : A × B) => (f ab.1, ab.2)) (fun (ab : A × B) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P ab.1) (Q ab.2)) cb = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (coarseOp f P cb.1) (Q cb.2)

noncomputable def MIPRE.Introspection.Honest.stopLabel {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] (S V : Finset ι) (a : (Fin (Fintype.card ↥S) → F) × (↥(V \ S) → F)) : HideLabel F ι

Equations

• MIPRE.Introspection.Honest.stopLabel S V a = (0, (MIPRE.Introspection.coordinateInsert S) a.1, MIPRE.Introspection.Honest.insertRegister (V \ S) a.2)

theorem MIPRE.Introspection.Honest.stopHideAnswer_split {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (S V : Finset ι) (h : S ⊆ V) (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (x : ↥V → F) : stopHideAnswer (CL.CLFun.cons S L next) V x = stopLabel S V ((CL.lperp (coordinateLinear L)) ((coordinateSplit S V h) x).1, ((coordinateSplit S V h) x).2)

theorem MIPRE.Introspection.Honest.stopHide_split {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (S V : Finset ι) (h : S ⊆ V) (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (a : HideLabel F ι) : stopHide (CL.CLFun.cons S L next) V a = registerOp (coordinateSplit S V h) (coarseOp (stopLabel S V) (fun (bt : (Fin (Fintype.card ↥S) → F) × (↥(V \ S) → F)) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Weyl.synOf Weyl.wX (⇑(CL.lperp (coordinateLinear L))) bt.1) (Weyl.proj Weyl.wX bt.2)) a)

Exact factorization of the stopping Hide measurement, with the actual dual map.