Replacing the state after Pauli extraction

For fixed projective measurements, changing two normalized state vectors by squared norm eta changes every test, and the whole game value, by at most 2 sqrt(eta). This supplies the actual value estimate used with the state approximation in introspection, in addition to its scalar error absorption.

In a bipartite model the second state is a vector φ of the model's Hilbert space, and the model with its state replaced by it is Ψ.withState φ (Phase 4 of planning/mipco-track.md).

theorem MIPRE.Introspection.qform_state_stability {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) (φ : Ψ.H) (hv : ‖Ψ.ψ‖ = 1) (hw : ‖φ‖ = 1) (R : 𝒞) (hR : Ψ.Bnd R 1) : |Ψ.qform R - (Ψ.withState φ).qform R| ≤ 2 * ‖Ψ.ψ - φ‖

A contraction's quadratic form is Lipschitz on the unit sphere.

theorem MIPRE.Introspection.pvm_event_bound {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {C : Type u_2} [Fintype C] [DecidableEq C] {M : C → 𝒞} (hM : IsPVMIn M) (s : Finset C) : Ψ.Bnd (∑ c ∈ s, M c) 1

The accepted effect of any event in a PVM is a contraction.

theorem MIPRE.Introspection.pvm_event_state_stability {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {C : Type u_2} [Fintype C] [DecidableEq C] (φ : Ψ.H) (hv : ‖Ψ.ψ‖ = 1) (hw : ‖φ‖ = 1) {M : C → 𝒞} (hM : IsPVMIn M) (s : Finset C) : |∑ c ∈ s, Ψ.qform (M c) - ∑ c ∈ s, (Ψ.withState φ).qform (M c)| ≤ 2 * ‖Ψ.ψ - φ‖

A change in state changes any PVM event by at most twice the vector distance.

theorem MIPRE.Introspection.testAcceptance_state_stability {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_6} {B : Type u_7} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (φ : Ψ.H) (hΨ : ‖Ψ.ψ‖ = 1) (hφ : ‖φ‖ = 1) (D : A → B → Bool) (M : A → 𝒜) (Q : B → ℬ) (hM : IsPVMIn M) (hQ : IsPVMIn Q) {η : ℝ} (hd : ‖Ψ.ψ - φ‖ ^ 2 ≤ η) : |testAcceptance Ψ D M Q - testAcceptance (Ψ.withState φ) D M Q| ≤ 2 * √η

State replacement for one concrete decision predicate.

theorem MIPRE.Introspection.povmValue_state_stability {𝒞 : 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} [Fintype X] [Fintype Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (G : Game X Y A B) (φ : Ψ.H) (hΨ : ‖Ψ.ψ‖ = 1) (hφ : ‖φ‖ = 1) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) (hMA : ∀ (x : X), IsPVMIn (MA x).op) (hMB : ∀ (y : Y), IsPVMIn (MB y).op) {η : ℝ} (hd : ‖Ψ.ψ - φ‖ ^ 2 ≤ η) : |Ψ.povmValue G MA MB - (Ψ.withState φ).povmValue G MA MB| ≤ 2 * √η

The full normalized question distribution preserves the same state-replacement bound.

theorem MIPRE.Introspection.povmValue_failure_transfer {𝒞 : 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} [Fintype X] [Fintype Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (G : Game X Y A B) (φ : Ψ.H) (hΨ : ‖Ψ.ψ‖ = 1) (hφ : ‖φ‖ = 1) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) (hMA : ∀ (x : X), IsPVMIn (MA x).op) (hMB : ∀ (y : Y), IsPVMIn (MB y).op) {ε η : ℝ} (hfail : 1 - Ψ.povmValue G MA MB ≤ ε) (hd : ‖Ψ.ψ - φ‖ ^ 2 ≤ η) : 1 - (Ψ.withState φ).povmValue G MA MB ≤ ε + 2 * √η

Transfer a game's failure bound to the nearby ideal state.