Sampling tests after answer coarse-graining

The selection probability is retained explicitly. The question map need not be injective: many sampler seeds may give the same question pair. Prefix coarse-graining is done on the acceptance predicate, before passing to squared distance, so no answer-fibre cardinality enters the error.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md).

theorem MIPRE.Introspection.agreement_subtest_average {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} {J : Type u_9} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype A] [Fintype B] [Fintype C] [DecidableEq C] [Fintype J] [DecidableEq J] (G : Game X Y A B) (hΨ : ‖Ψ.ψ‖ = 1) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue G MA MB ≤ ε) (D : J → ℝ) (hD : ∀ (j : J), 0 ≤ D j) (q : J → X × Y) {c : ℝ} (hc : 0 < c) (hpush : ∀ (p : X × Y), c * ∑ j : J with q j = p, D j ≤ G.μ p.1 p.2) (f : J → A → C) (g : J → B → C) (hcheck : ∀ (j : J) (a : A) (b : B), G.D (q j).1 (q j).2 a b = true → f j a = g j b) : ∑ j : J, D j * ∑ z : C, Ψ.xSqNorm ((POVMIn.map (f j) (MA (q j).1)).op z) ((POVMIn.map (g j) (MB (q j).2)).op z) ≤ 2 * (ε / c)

A tested equality of processed answers gives averaged cross-party closeness, including all output values of the processing maps.

theorem MIPRE.Introspection.sampling_pauli_estimate {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} {J : Type u_9} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype A] [Fintype B] [Fintype C] [DecidableEq C] [Fintype J] [DecidableEq J] (G : Game X Y A B) (hΨ : ‖Ψ.ψ‖ = 1) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue G MA MB ≤ ε) (D : J → ℝ) (hD : ∀ (j : J), 0 ≤ D j) (q : J → X × Y) {c : ℝ} (hc : 0 < c) (hpush : ∀ (p : X × Y), c * ∑ j : J with q j = p, D j ≤ G.μ p.1 p.2) (f : J → A → C) (g : J → B → C) (hcheck : ∀ (j : J) (a : A) (b : B), G.D (q j).1 (q j).2 a b = true → f j a = g j b) (P : J → C → 𝒜) {η : ℝ} (hP : ∑ j : J, D j * ∑ z : C, Ψ.stateSqNorm (P j z - (POVMIn.map (f j) (MA (q j).1)).op z) ≤ η) : ∑ j : J, D j * ∑ z : C, Ψ.xSqNorm (P j z) ((POVMIn.map (g j) (MB (q j).2)).op z) ≤ 2 * η + 4 * (ε / c)

The Pauli sampling test remains sound after replacing the tested Pauli measurement by its ideal one. The explicit loss is 2 η + 4 ε / c.

theorem MIPRE.Introspection.sampling_prefix_estimate {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {J : Type u_9} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype J] [DecidableEq J] {F : Type u_10} {ι : Type u_11} {O : Type u_12} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype O] [DecidableEq O] {ℓ : ℕ} (G : Game X Y ((ι → F) × O) ((ι → F) × O)) (hΨ : ‖Ψ.ψ‖ = 1) (MA : X → POVMIn ((ι → F) × O) 𝒜) (MB : Y → POVMIn ((ι → F) × O) ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue G MA MB ≤ ε) (D : J → ℝ) (hD : ∀ (j : J), 0 ≤ D j) (q : J → X × Y) {c : ℝ} (hc : 0 < c) (hpush : ∀ (p : X × Y), c * ∑ j : J with q j = p, D j ≤ G.μ p.1 p.2) (P : J → CL.CLFun F ι ℓ) (hP : ∀ (j : J), (P j).SupportedOn Finset.univ) (hcheck : ∀ (j : J) (a b : (ι → F) × O), G.D (q j).1 (q j).2 a b = true → a = ((P j).eval b.1, b.2)) (k : ℕ) : ∑ j : J, D j * ∑ z : (ι → F) × O, Ψ.xSqNorm ((POVMIn.map (fun (a : (ι → F) × O) => ((P j).outputPrefix k a.1, a.2)) (MA (q j).1)).op z) ((POVMIn.map (fun (b : (ι → F) × O) => ((CL.CLFun.truncate k (P j)).eval b.1, b.2)) (MB (q j).2)).op z) ≤ 2 * (ε / c)

The introspection sampling test, at every CL prefix. The output sum is over the entire ambient answer alphabet, including vectors outside the marginal CL image.

theorem MIPRE.Introspection.mapped_operator_zero_of_not_range {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {B : Type u_7} {C : Type u_8} [Fintype B] [Fintype C] [DecidableEq C] (N : POVMIn B ℬ) (g : B → C) {z : C} (hz : z ∉ Set.range g) : (POVMIn.map g N).op z = 0

A coarse-grained outcome outside the image has exactly the zero operator.

theorem MIPRE.Introspection.off_range_weight_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {B : Type u_7} {C : Type u_8} [Fintype B] [Fintype C] [DecidableEq C] (M : POVMIn C 𝒜) (N : POVMIn B ℬ) (g : B → C) : ∑ z : C with z ∉ Set.range g, Ψ.stateSqNorm (M.op z) ≤ ∑ z : C, Ψ.xSqNorm (M.op z) ((POVMIn.map g N).op z)

The consistency estimate controls the total squared weight of all impossible answers. No restriction to the honest image is made in a later use of the sampling estimate.