Value stability for the introspection induction

The induction replaces projective measurements using summed squared state distance. The resulting change in test acceptance is dimension independent: 2 sqrt(delta) per party. Summing outcomes before Cauchy--Schwarz avoids any loss depending on the size of the introspection answer alphabet.

Everything is stated in a bipartite model (Phase 4 of planning/mipco-track.md): the single-state facts for a state model Ψ, the facts about tests for a bipartite model Ψ, the model playing the part of the state vector of the matrix analysis.

theorem MIPRE.Introspection.pvm_subset_mass {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {C : Type u_2} [Fintype C] (hv : ‖Ψ.ψ‖ = 1) {M : C → 𝒞} (hM : IsPVMIn M) (s : Finset C) : ∑ c ∈ s, Ψ.snorm (M c) ^ 2 ≤ 1

A subset of the outcomes of a projective measurement has squared mass at most one.

theorem MIPRE.Introspection.abs_sum_qform_mul_le {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {C : Type u_2} [Fintype C] (s : Finset C) (M R : C → 𝒞) (hM : ∀ (c : C), star (M c) = M c) : |∑ c ∈ s, Ψ.qform (M c * R c)| ≤ √(∑ c ∈ s, Ψ.snorm (M c) ^ 2) * √(∑ c ∈ s, Ψ.snorm (R c) ^ 2)

Cauchy--Schwarz for a selected set of outcome-indexed operator products.

theorem MIPRE.Introspection.pvm_event_stability {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {C : Type u_2} [Fintype C] (hv : ‖Ψ.ψ‖ = 1) {M R : C → 𝒞} (hM : IsPVMIn M) (hR : IsPVMIn R) (s : Finset C) {δ : ℝ} (hd : ∑ c : C, Ψ.snorm (M c - R c) ^ 2 ≤ δ) : |∑ c ∈ s, Ψ.qform (M c) - ∑ c ∈ s, Ψ.qform (R c)| ≤ 2 * √δ

Changing a projective measurement by squared distance delta changes the probability of any event by at most 2 sqrt(delta), with no outcome-count factor.

theorem MIPRE.Introspection.joint_isPVM {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {B : Type u_5} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (M : A → 𝒜) (Q : B → ℬ) (hM : IsPVMIn M) (hQ : IsPVMIn Q) : IsPVMIn fun (ab : A × B) => Ψ.πA (M ab.1) * Ψ.πB (Q ab.2)

Independent local projective measurements give a projective measurement of both answers.

theorem MIPRE.Introspection.joint_distance_left {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {B : Type u_5} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (M R : A → 𝒜) (Q : B → ℬ) (hQ : IsPVMIn Q) : ∑ ab : A × B, Ψ.snorm (Ψ.πA (M ab.1) * Ψ.πB (Q ab.2) - Ψ.πA (R ab.1) * Ψ.πB (Q ab.2)) ^ 2 = ∑ a : A, Ψ.stateSqNorm (M a - R a)

Summing the unchanged party's projective outcomes removes that party from the error.

def MIPRE.Introspection.testAcceptance {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (D : A → B → Bool) (M : A → 𝒜) (Q : B → ℬ) : ℝ

The acceptance functional of one test on bare local measurement families.

Equations

• MIPRE.Introspection.testAcceptance Ψ D M Q = ∑ a : A, ∑ b : B, (if D a b = true then 1 else 0) * Ψ.bornProb (M a) (Q b)

theorem MIPRE.Introspection.testAcceptance_stability_left {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {B : Type u_5} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (hΨ : ‖Ψ.ψ‖ = 1) (D : A → B → Bool) (M R : A → 𝒜) (Q : B → ℬ) (hM : IsPVMIn M) (hR : IsPVMIn R) (hQ : IsPVMIn Q) {δ : ℝ} (hd : ∑ a : A, Ψ.stateSqNorm (M a - R a) ≤ δ) : |testAcceptance Ψ D M Q - testAcceptance Ψ D R Q| ≤ 2 * √δ

One player's projective replacement changes any test by at most 2 sqrt(delta).

theorem MIPRE.Introspection.testAcceptance_swap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {B : Type u_5} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (D : A → B → Bool) (M : A → 𝒜) (Q : B → ℬ) : testAcceptance Ψ.swap (fun (b : B) (a : A) => D a b) Q M = testAcceptance Ψ D M Q

Swapping the two parties preserves test acceptance with the predicate arguments swapped.

theorem MIPRE.Introspection.testAcceptance_stability_right {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {B : Type u_5} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (hΨ : ‖Ψ.ψ‖ = 1) (D : A → B → Bool) (M : A → 𝒜) (Q R : B → ℬ) (hM : IsPVMIn M) (hQ : IsPVMIn Q) (hR : IsPVMIn R) {δ : ℝ} (hd : ∑ b : B, Ψ.swap.stateSqNorm (Q b - R b) ≤ δ) : |testAcceptance Ψ D M Q - testAcceptance Ψ D M R| ≤ 2 * √δ

The corresponding replacement estimate on Bob's side, with its actual state norm.

theorem MIPRE.Introspection.testAcceptance_stability {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {B : Type u_5} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (hΨ : ‖Ψ.ψ‖ = 1) (D : A → B → Bool) (M R : A → 𝒜) (Q T : B → ℬ) (hM : IsPVMIn M) (hR : IsPVMIn R) (hQ : IsPVMIn Q) (hT : IsPVMIn T) {δA δB : ℝ} (hA : ∑ a : A, Ψ.stateSqNorm (M a - R a) ≤ δA) (hB : ∑ b : B, Ψ.swap.stateSqNorm (Q b - T b) ≤ δB) : |testAcceptance Ψ D M Q - testAcceptance Ψ D R T| ≤ 2 * √δA + 2 * √δB

Replacing both local PVMs costs the sum of their square-root errors.