Projectivizing a conditional residual measurement

One fixed ancilla is added on the residual side of every prefix. The prefix projectors are unchanged. Squared distance to the old projective measurement costs 2 sqrt(delta); a dilation does not in general preserve that distance.

In a bipartite model (Phase 4 of planning/mipco-track.md): the ancilla is the first player's one-sided extension Ψ.expandA t₀ (MIPRE/Foundations/AncillaDilation.lean), an old operator m becomes m ⊗ 1, and the dilation of the residual POVMs is MIPRE.exists_pvm_dilation, in the first player's algebra and against the fixed basis vector t₀ = inl (a₀, 0) of the ancilla DilationAncilla A K, the number K of Kraus terms depending on the POVMs.

theorem MIPRE.Introspection.stateSqNorm_expandA_diagonal {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {T : Type u_5} [Fintype T] [DecidableEq T] (t₀ : T) (m : 𝒜) : (Ψ.expandA t₀).stateSqNorm (Matrix.diagonal fun (x : T) => m) = Ψ.stateSqNorm m

Extending an old operator by identity preserves its state norm exactly.

theorem MIPRE.Introspection.qform_πA_expandA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {T : Type u_5} [Fintype T] [DecidableEq T] (t₀ : T) (X : Matrix T T 𝒜) : (Ψ.expandA t₀).qform ((Ψ.expandA t₀).πA X) = Ψ.qform (Ψ.πA (X t₀ t₀))

The first player's quadratic form on the one-sided extension is that of the (t₀, t₀) entry.

theorem MIPRE.Introspection.dilated_pvm_distance {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} {T : Type u_5} [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] (hΨ : ‖Ψ.ψ‖ = 1) (t₀ : T) (M R : A → 𝒜) (P : A → Matrix T T 𝒜) (hM : IsPVMIn M) (hP : IsPVMIn P) (hk : ∀ (a : A), P a t₀ t₀ = R a) {δ : ℝ} (hd : ∑ a : A, Ψ.stateSqNorm (M a - R a) ≤ δ) : ∑ a : A, (Ψ.expandA t₀).stateSqNorm ((Matrix.diagonal fun (x : T) => M a) - P a) ≤ 2 * √δ

A fixed-state projective dilation remains close to an old PVM. The bound is uniform over every dilation with the displayed compression identity.

def MIPRE.Introspection.conditionalDilationOp {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] {I : Type u_2} {Y : Type u_3} {A : Type u_4} {T : Type u_5} (Z : Y → Matrix I I ℂ) (P : Y → A → Matrix T T 𝒜) (p : Y × A) : Matrix T T (Matrix I I 𝒜)

The joint operator: the prefix projector of the register times the dilated residual operator, with the fresh ancilla outermost, as the one-sided extension carries it.

Equations

• MIPRE.Introspection.conditionalDilationOp Z P p = (P p.1 p.2).map fun (x : 𝒜) => MIPRE.smulKron x (Z p.1)

theorem MIPRE.Introspection.conditionalDilationOp_isPVM {𝒜 : Type u_1} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {I : Type u_2} {Y : Type u_3} {A : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] (Z : Y → Matrix I I ℂ) (hZ : IsPVM Z) (P : Y → A → Matrix T T 𝒜) (hP : ∀ (y : Y), IsPVMIn (P y)) : IsPVMIn (conditionalDilationOp Z P)

Conditional projective residual measurements keep the joint measurement projective while leaving every prefix projector untouched.

theorem MIPRE.Introspection.conditionalDilationOp_compress {𝒜 : Type u_1} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {I : Type u_2} {Y : Type u_3} {A : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] (t₀ : T) (Z : Y → Matrix I I ℂ) (P : Y → A → Matrix T T 𝒜) (R : Y → A → 𝒜) (hk : ∀ (y : Y) (a : A), P y a t₀ t₀ = R y a) (p : Y × A) : conditionalDilationOp Z P p t₀ t₀ = smulKron (R p.1 p.2) (Z p.1)

The full conditional dilation compresses to the desired prefix times residual POVM, using the same fixed vector for every prefix and outcome.

theorem MIPRE.Introspection.conditionalDilationOp_born {𝒜 : Type u_1} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {I : Type u_2} {Y : Type u_3} {A : Type u_4} {T : Type u_5} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] {𝒞 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 (Matrix I I 𝒜) ℬ) (t₀ : T) (Z : Y → Matrix I I ℂ) (P : Y → A → Matrix T T 𝒜) (R : Y → A → 𝒜) (hk : ∀ (y : Y) (a : A), P y a t₀ t₀ = R y a) (p : Y × A) (b : ℬ) : (Ψ.expandA t₀).bornProb (conditionalDilationOp Z P p) b = Ψ.bornProb (smulKron (R p.1 p.2) (Z p.1)) b

The conditional product form has exactly the original outcome probabilities against every measurement on the other party.

theorem MIPRE.Introspection.exists_conditional_projective_dilation {𝒜 : Type u_1} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {I : Type u_2} {Y : Type u_3} {A : Type u_4} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] {𝒞 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {J : Type u_8} [Fintype J] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (Ψ : BipartiteModel 𝒞 (Matrix I I 𝒜) ℬ) (hΨ : ‖Ψ.ψ‖ = 1) (a₀ : A) (D : J → ℝ) (hD0 : ∀ (j : J), 0 ≤ D j) (hD1 : ∑ j : J, D j = 1) (Z : J → Y → Matrix I I ℂ) (hZ : ∀ (j : J), IsPVM (Z j)) (Q : J → Y → POVMIn A 𝒜) (M : J → Y × A → Matrix I I 𝒜) (hM : ∀ (j : J), IsPVMIn (M j)) {δ : ℝ} (hd : ∑ j : J, D j * ∑ p : Y × A, Ψ.stateSqNorm (M j p - smulKron ((Q j p.1).op p.2) (Z j p.1)) ≤ δ) : ∃ (K : ℕ) (P : J → Y → A → Matrix (DilationAncilla A K) (DilationAncilla A K) 𝒜), (∀ (j : J) (y : Y), IsPVMIn (P j y)) ∧ (∀ (j : J) (y : Y) (a : A), P j y a (Sum.inl (a₀, 0)) (Sum.inl (a₀, 0)) = (Q j y).op a) ∧ (∀ (j : J), IsPVMIn (conditionalDilationOp (Z j) (P j))) ∧ (∀ (j : J) (p : Y × A), conditionalDilationOp (Z j) (P j) p (Sum.inl (a₀, 0)) (Sum.inl (a₀, 0)) = smulKron ((Q j p.1).op p.2) (Z j p.1)) ∧ ∑ j : J, D j * ∑ p : Y × A, (Ψ.expandA (Sum.inl (a₀, 0))).stateSqNorm ((Matrix.diagonal fun (x : DilationAncilla A K) => M j p) - conditionalDilationOp (Z j) (P j) p) ≤ 2 * √δ

Common-ancilla conditional projectivization. All residual POVMs in a question/prefix family are dilated with one fixed ancilla state. The resulting joint PVMs retain the displayed prefix projectors and are quantitatively close to the old projective family on the one extended state.

theorem MIPRE.Introspection.exists_varying_conditional_projective_dilation {J : Type u_1} {A : Type u_2} [Fintype J] [Fintype A] [DecidableEq A] {I : J → Type u_3} {Y : J → Type u_4} [(j : J) → Fintype (I j)] [(j : J) → DecidableEq (I j)] [(j : J) → Fintype (Y j)] [(j : J) → DecidableEq (Y j)] {𝒞 : J → Type u_5} {𝒜 : J → Type u_6} {ℬ : J → Type u_7} [(j : J) → Ring (𝒞 j)] [(j : J) → StarRing (𝒞 j)] [(j : J) → Algebra ℂ (𝒞 j)] [(j : J) → Ring (𝒜 j)] [(j : J) → StarRing (𝒜 j)] [(j : J) → Algebra ℂ (𝒜 j)] [∀ (j : J), StarModule ℂ (𝒜 j)] [(j : J) → PartialOrder (𝒜 j)] [∀ (j : J), StarOrderedRing (𝒜 j)] [∀ (j : J), StarProper (𝒜 j)] [(j : J) → Ring (ℬ j)] [(j : J) → StarRing (ℬ j)] [(j : J) → Algebra ℂ (ℬ j)] (Ψ : (j : J) → BipartiteModel (𝒞 j) (Matrix (I j) (I j) (𝒜 j)) (ℬ j)) (hΨ : ∀ (j : J), ‖(Ψ j).ψ‖ = 1) (a₀ : A) (D : J → ℝ) (hD0 : ∀ (j : J), 0 ≤ D j) (hD1 : ∑ j : J, D j = 1) (Z : (j : J) → Y j → Matrix (I j) (I j) ℂ) (hZ : ∀ (j : J), IsPVM (Z j)) (Q : (j : J) → Y j → POVMIn A (𝒜 j)) (M : (j : J) → Y j × A → Matrix (I j) (I j) (𝒜 j)) (hM : ∀ (j : J), IsPVMIn (M j)) {δ : ℝ} (hd : ∑ j : J, D j * ∑ p : Y j × A, (Ψ j).stateSqNorm (M j p - smulKron ((Q j p.1).op p.2) (Z j p.1)) ≤ δ) : ∃ (K : J → ℕ) (P : (j : J) → Y j → A → Matrix (DilationAncilla A (K j)) (DilationAncilla A (K j)) (𝒜 j)), (∀ (j : J) (y : Y j), IsPVMIn (P j y)) ∧ (∀ (j : J) (y : Y j) (a : A), P j y a (Sum.inl (a₀, 0)) (Sum.inl (a₀, 0)) = (Q j y).op a) ∧ (∀ (j : J), IsPVMIn (conditionalDilationOp (Z j) (P j))) ∧ (∀ (j : J) (p : Y j × A), conditionalDilationOp (Z j) (P j) p (Sum.inl (a₀, 0)) (Sum.inl (a₀, 0)) = smulKron ((Q j p.1).op p.2) (Z j p.1)) ∧ ∑ j : J, D j * ∑ p : Y j × A, ((Ψ j).expandA (Sum.inl (a₀, 0))).stateSqNorm ((Matrix.diagonal fun (x : DilationAncilla A (K j)) => M j p) - conditionalDilationOp (Z j) (P j) p) ≤ 2 * √δ

Conditional projectivization with varying local registers. The prefix, residual and other-party carriers may all depend on the conditioned question, and so may the models. Each question gets one fixed ancilla state, common to all its prefixes; its number of Kraus terms depends on the question.