The cost of completing isometric image measurements

The extracted ideal state need not lie exactly in the isometries' images. Its image-complement mass is bounded by its squared distance to the actual embedded state. Completing an image PVM at one outcome therefore adds only a dimension-independent error, even when primitive estimates are stated on the ideal state.

Stated for a local isometry Φ : LocalIsometry M M' of bipartite models (Phase 4 of planning/mipco-track.md): the ideal state is the target's state M'.ψ, the embedded state is Φ.W M.ψ, the image of an operator is Φ.ΦA, its complement 1 - Φ.ΦA 1, and the completed measurement is the transport Φ.transportOpA (MIPRE/Foundations/LocalIsometry.lean).

theorem MIPRE.Introspection.projector_mass_le_state_distance {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) (v : Ψ.H) (C : 𝒞) (hC : star C = C) (hCC : C * C = C) (hz : (Ψ.π C) v = 0) : Ψ.snorm C ^ 2 ≤ ‖v - Ψ.ψ‖ ^ 2

A projection annihilating one vector has at most the squared vector distance as its mass on the state. Normalization is not required.

theorem MIPRE.Introspection.transportA_map_op {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {A : Type u_7} {B : Type u_8} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] (a₀ : A) (P : POVMIn A 𝒜) (hP : IsPVMIn P.op) (f : A → B) (b : B) : (POVMIn.map f (Φ.transportA a₀ P hP)).op b = Φ.transportOpA (f a₀) (POVMIn.map f P).op b

Coarse-graining a completed image measurement is the image of the coarse-graining, with the same complement placed at the mapped default.

theorem MIPRE.Introspection.isometricComplement_alice_mass {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : M'.snorm (M'.πA (1 - Φ.ΦA 1)) ^ 2 ≤ ‖Φ.W M.ψ - M'.ψ‖ ^ 2

theorem MIPRE.Introspection.isometricComplement_bob_mass {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : M'.snorm (M'.πB (1 - Φ.ΦB 1)) ^ 2 ≤ ‖Φ.W M.ψ - M'.ψ‖ ^ 2

theorem MIPRE.Introspection.isometricEffect_alice_completion_error {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {A : Type u_7} [Fintype A] [DecidableEq A] (a₀ : A) (P : A → 𝒜) : ∑ a : A, M'.snorm (M'.πA (Φ.transportOpA a₀ P a - Φ.ΦA (P a))) ^ 2 = M'.snorm (M'.πA (1 - Φ.ΦA 1)) ^ 2

Exactly one outcome receives the image complement.

theorem MIPRE.Introspection.isometricEffect_alice_error_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {A : Type u_7} [Fintype A] [DecidableEq A] (a₀ : A) (P : A → 𝒜) (Q : A → 𝒜') {δ η : ℝ} (hδ : ∑ a : A, M'.snorm (M'.πA (Φ.ΦA (P a) - Q a)) ^ 2 ≤ δ) (hη : ‖Φ.W M.ψ - M'.ψ‖ ^ 2 ≤ η) : ∑ a : A, M'.snorm (M'.πA (Φ.transportOpA a₀ P a - Q a)) ^ 2 ≤ 2 * δ + 2 * η

Primitive ideal-state image estimates survive completing the measurement to a normalized PVM, with no factor for the number of outcomes.

theorem MIPRE.Introspection.isometricEffect_bob_error_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {B : Type u_7} [Fintype B] [DecidableEq B] (b₀ : B) (Q : B → ℬ) (R : B → ℬ') {δ η : ℝ} (hδ : ∑ b : B, M'.snorm (M'.πB (Φ.ΦB (Q b) - R b)) ^ 2 ≤ δ) (hη : ‖Φ.W M.ψ - M'.ψ‖ ^ 2 ≤ η) : ∑ b : B, M'.snorm (M'.πB (Φ.swap.transportOpA b₀ Q b - R b)) ^ 2 ≤ 2 * δ + 2 * η