Transferring projective measurement errors between nearby states

The summed squared distance of two PVMs on a new state is at most twice its old value plus eight times the squared vector distance. PVM normalization removes any dependence on the number of outcomes. The state vectors need not be normalized. Alice and Bob forms expose the estimate in the conventions used by the extracted Pauli guarantees.

Stated in a model (Phase 4 of planning/mipco-track.md): the old state is the model's own, the new state φ is any vector of its Hilbert space, and the model at the new state is Ψ.withState φ.

theorem MIPRE.Introspection.snorm_one_eq_norm {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) : Ψ.snorm 1 = ‖Ψ.ψ‖

The identity's state norm is the norm of the state.

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

The total squared PVM mass on any vector is its squared norm.

theorem MIPRE.Introspection.sum_pvm_difference_snorm_sq_le {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {C : Type u_2} [Fintype C] {M R : C → 𝒞} (hM : IsPVMIn M) (hR : IsPVMIn R) : ∑ c : C, Ψ.snorm (M c - R c) ^ 2 ≤ 4 * ‖Ψ.ψ‖ ^ 2

Two PVMs have summed squared difference at most four times the state's squared norm, without an outcome-count factor.

theorem MIPRE.Introspection.snorm_state_sq_le {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) (φ : Ψ.H) (R : 𝒞) : (Ψ.withState φ).snorm R ^ 2 ≤ 2 * Ψ.snorm R ^ 2 + 2 * (Ψ.withState (Ψ.ψ - φ)).snorm R ^ 2

A single operator's squared state norm splits with coefficient two when the state vector changes.

theorem MIPRE.Introspection.sum_snorm_state_transfer {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {C : Type u_2} [Fintype C] (φ : Ψ.H) {M R : C → 𝒞} (hM : IsPVMIn M) (hR : IsPVMIn R) : ∑ c : C, (Ψ.withState φ).snorm (M c - R c) ^ 2 ≤ 2 * ∑ c : C, Ψ.snorm (M c - R c) ^ 2 + 8 * ‖Ψ.ψ - φ‖ ^ 2

Transfer the summed squared difference of two projective measurements to a nearby state. No unit-state assumptions are needed.

theorem MIPRE.Introspection.sum_stateSqNorm_state_transfer {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {C : Type u_4} [Fintype C] (φ : Ψ.H) {M R : C → 𝒜} (hM : IsPVMIn M) (hR : IsPVMIn R) : ∑ c : C, (Ψ.withState φ).stateSqNorm (M c - R c) ≤ 2 * ∑ c : C, Ψ.stateSqNorm (M c - R c) + 8 * ‖Ψ.ψ - φ‖ ^ 2

Alice's local PVM error transfers between arbitrary vectors.

theorem MIPRE.Introspection.sum_stateSqNorm_state_transfer_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {C : Type u_4} [Fintype C] (φ : Ψ.H) {M R : C → 𝒜} (hM : IsPVMIn M) (hR : IsPVMIn R) {δ η : ℝ} (hδ : ∑ c : C, Ψ.stateSqNorm (M c - R c) ≤ δ) (hdist : ‖Ψ.ψ - φ‖ ^ 2 ≤ η) : ∑ c : C, (Ψ.withState φ).stateSqNorm (M c - R c) ≤ 2 * δ + 8 * η

Transfer a bounded Alice PVM approximation to the extracted state.

theorem MIPRE.Introspection.sum_bob_snorm_state_transfer {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {C : Type u_4} [Fintype C] (φ : Ψ.H) {M R : C → ℬ} (hM : IsPVMIn M) (hR : IsPVMIn R) : ∑ c : C, (Ψ.withState φ).snorm (Ψ.πB (M c - R c)) ^ 2 ≤ 2 * ∑ c : C, Ψ.snorm (Ψ.πB (M c - R c)) ^ 2 + 8 * ‖Ψ.ψ - φ‖ ^ 2

Bob's local PVM error transfers with the same constants.

theorem MIPRE.Introspection.sum_bob_snorm_state_transfer_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {C : Type u_4} [Fintype C] (φ : Ψ.H) {M R : C → ℬ} (hM : IsPVMIn M) (hR : IsPVMIn R) {δ η : ℝ} (hδ : ∑ c : C, Ψ.snorm (Ψ.πB (M c - R c)) ^ 2 ≤ δ) (hdist : ‖Ψ.ψ - φ‖ ^ 2 ≤ η) : ∑ c : C, (Ψ.withState φ).snorm (Ψ.πB (M c - R c)) ^ 2 ≤ 2 * δ + 8 * η

Transfer a bounded Bob PVM approximation to the extracted state.