Recovering all outcomes from valid-outcome extraction estimates

Pauli extraction sums only the valid full-register answers. The actual introspection induction also retains every malformed answer. Positivity and the submeasurement mass estimate extend the former guarantee to the whole mapped alphabet, without an answer-cardinality factor or a premise that malformed effects vanish.

Stated for a state model, with positivity on the represented operators, and for a local isometry of bipartite models (Phase 4 of planning/mipco-track.md).

theorem MIPRE.Introspection.submeasurement_extension_mass {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {A : Type u_2} [Fintype A] [DecidableEq A] (hΨ : ‖Ψ.ψ‖ = 1) (M C : A → 𝒞) (hM : ∀ (a : A), 0 ≤ Ψ.π (M a)) (hC : ∀ (a : A), 0 ≤ Ψ.π (C a)) (hCsum : ∑ a : A, Ψ.π (C a) ≤ 1) (hMC : ∀ (a : A), Ψ.π (M a) ≤ Ψ.π (C a)) : ∑ a : A, Ψ.snorm (M a - C a) ^ 2 ≤ 1 - ∑ a : A, Ψ.qform (M a)

Extending a positive submeasurement inside another submeasurement costs at most the missing mass. Normalization of the extension is not needed.

theorem MIPRE.Introspection.submeasurement_extension_dist {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {A : Type u_2} [Fintype A] [DecidableEq A] (hΨ : ‖Ψ.ψ‖ = 1) (P M C : A → 𝒞) (hP : IsPVMIn P) (hM : ∀ (a : A), 0 ≤ Ψ.π (M a)) (hC : ∀ (a : A), 0 ≤ Ψ.π (C a)) (hCsum : ∑ a : A, Ψ.π (C a) ≤ 1) (hMC : ∀ (a : A), Ψ.π (M a) ≤ Ψ.π (C a)) {δ : ℝ} (hclose : ∑ a : A, Ψ.snorm (P a - M a) ^ 2 ≤ δ) : ∑ a : A, Ψ.snorm (P a - C a) ^ 2 ≤ 2 * δ + 4 * √δ

A nearby positive submeasurement may be extended arbitrarily inside the identity with the same dimension-independent completion bound.

theorem MIPRE.Introspection.valid_outcome_error_le {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {A : Type u_2} {B : Type u_3} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (hΨ : ‖Ψ.ψ‖ = 1) (M : B → 𝒞) (hM : ∀ (b : B), 0 ≤ Ψ.π (M b)) (hMsum : ∑ b : B, Ψ.π (M b) ≤ 1) (f : B → Option A) (v : A → B) (hv : ∀ (a : A), f (v a) = some a) (P : Option A → 𝒞) (hP : IsPVMIn P) (hPnone : P none = 0) {δ : ℝ} (hclose : ∑ a : A, Ψ.snorm (M (v a) - P (some a)) ^ 2 ≤ δ) : ∑ a : Option A, Ψ.snorm (fibSumIn M f a - P a) ^ 2 ≤ 2 * δ + 4 * √δ

Closeness on one correctly labelled raw answer for each valid outcome controls the complete coarse measurement, including all malformed answers. The ideal measurement has zero effect at the explicit malformed outcome.

theorem MIPRE.Introspection.π_πA_ΦA_one_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 ℂ ℬ'] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : M'.π (M'.πA (Φ.ΦA 1)) ≤ 1

The image of the unit is represented below the identity.

theorem MIPRE.Introspection.isometric_valid_outcome_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 ℂ ℬ'] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {A : Type u_7} {B : Type u_8} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (hM' : ‖M'.ψ‖ = 1) (N : POVMIn B 𝒜) (f : B → Option A) (v : A → B) (hv : ∀ (a : A), f (v a) = some a) (P : Option A → 𝒜') (hP : IsPVMIn P) (hPnone : P none = 0) {δ : ℝ} (hclose : ∑ a : A, M'.snorm (M'.πA (Φ.ΦA (N.op (v a)) - P (some a))) ^ 2 ≤ δ) : ∑ a : Option A, M'.snorm (M'.πA (Φ.ΦA ((POVMIn.map f N).op a) - P a)) ^ 2 ≤ 2 * δ + 4 * √δ

Valid raw-answer estimates for an isometric image imply the complete mapped estimate on Alice, including the explicit malformed outcome.

theorem MIPRE.Introspection.isometric_valid_outcome_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 ℂ ℬ'] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] {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 ℬ'] (hM' : ‖M'.ψ‖ = 1) (N : POVMIn B ℬ) (f : B → Option A) (v : A → B) (hv : ∀ (a : A), f (v a) = some a) (P : Option A → ℬ') (hP : IsPVMIn P) (hPnone : P none = 0) {δ : ℝ} (hclose : ∑ a : A, M'.snorm (M'.πB (Φ.ΦB (N.op (v a)) - P (some a))) ^ 2 ≤ δ) : ∑ a : Option A, M'.snorm (M'.πB (Φ.ΦB ((POVMIn.map f N).op a) - P a)) ^ 2 ≤ 2 * δ + 4 * √δ

The corresponding full-outcome estimate on Bob.