Hiding-test chains after coarse-graining consistency

Coarse-graining is performed on the tests' accepted-answer relations. Only then are the two cross-party estimates combined into a same-side estimate. This is the order required to avoid the exponentially large fibre loss discussed in the paper's corrected proof of lem:intro-sound-2.

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

theorem MIPRE.Introspection.operator_chain_telescope {R : Type u_1} [AddCommGroup R] (P : ℕ → R) (n : ℕ) : ∑ i ∈ Finset.range n, (P i - P (i + 1)) = P 0 - P n

Telescoping the consecutive differences of a finite operator chain.

theorem MIPRE.Introspection.same_side_via_common_other {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {C : Type u_8} [Fintype C] [DecidableEq C] (P Q : C → 𝒜) (R : C → ℬ) : ∑ z : C, Ψ.stateSqNorm (P z - Q z) ≤ 2 * ∑ z : C, Ψ.xSqNorm (P z) (R z) + 2 * ∑ z : C, Ψ.xSqNorm (Q z) (R z)

Two measurements consistent with the same opposite-party measurement are close on their own side. There is no outcome-cardinality factor.

theorem MIPRE.Introspection.hiding_same_side_estimate {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : 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] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (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₁ q₂ : J → X × Y) (hBob : ∀ (j : J), (q₁ j).2 = (q₂ j).2) {c₁ c₂ : ℝ} (hc₁ : 0 < c₁) (hc₂ : 0 < c₂) (hpush₁ : ∀ (p : X × Y), c₁ * ∑ j : J with q₁ j = p, D j ≤ G.μ p.1 p.2) (hpush₂ : ∀ (p : X × Y), c₂ * ∑ j : J with q₂ j = p, D j ≤ G.μ p.1 p.2) (f₁ 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) (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, Ψ.stateSqNorm ((POVMIn.map (f₁ j) (MA (q₁ j).1)).op z - (POVMIn.map (f₂ j) (MA (q₂ j).1)).op z) ≤ 4 * (ε / c₁) + 4 * (ε / c₂)

The hiding-same test and the common-type consistency test give the required same-side marginal relation, with explicit loss 4ε/c₁ + 4ε/c₂.

theorem MIPRE.Introspection.stateSqNorm_hiding_chain {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (P : ℕ → 𝒜) (n : ℕ) : Ψ.stateSqNorm (P 0 - P n) ≤ ↑n * ∑ i ∈ Finset.range n, Ψ.stateSqNorm (P i - P (i + 1))

A chain of n hiding levels costs n times the sum of its squared edge errors.

theorem MIPRE.Introspection.hiding_chain_average {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {C : Type u_8} {J : Type u_9} [Fintype C] [DecidableEq C] [Fintype J] [DecidableEq J] (D : J → ℝ) (hD : ∀ (j : J), 0 ≤ D j) (P : ℕ → J → C → 𝒜) (n : ℕ) (δ : ℕ → ℝ) (hstep : ∀ i < n, ∑ j : J, D j * ∑ z : C, Ψ.stateSqNorm (P i j z - P (i + 1) j z) ≤ δ i) : ∑ j : J, D j * ∑ z : C, Ψ.stateSqNorm (P 0 j z - P n j z) ≤ ↑n * ∑ i ∈ Finset.range n, δ i

The averaged hiding chain, with one error bound per edge and no dependence on the number of outcomes or sampled question seeds.

theorem MIPRE.Introspection.hiding_chain_uniform {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {C : Type u_8} {J : Type u_9} [Fintype C] [DecidableEq C] [Fintype J] [DecidableEq J] (D : J → ℝ) (hD : ∀ (j : J), 0 ≤ D j) (P : ℕ → J → C → 𝒜) (n : ℕ) {δ : ℝ} (hstep : ∀ i < n, ∑ j : J, D j * ∑ z : C, Ψ.stateSqNorm (P i j z - P (i + 1) j z) ≤ δ) : ∑ j : J, D j * ∑ z : C, Ψ.stateSqNorm (P 0 j z - P n j z) ≤ ↑n ^ 2 * δ

With a uniform edge bound, the total hiding-chain error is at most n² δ.