Projective dilation against a fixed state, in any star-ordered ring

Introspection's adaptive inductions dilate a family of positive operator valued measures to projective ones against one fixed ancilla state, common to the whole family: the matrix proof uses exists_projective_dilation (MIPRE/Foundations/Dilation.lean), a unitary extension in finite dimension. Phase 4 of planning/mipco-track.md needs the same in a player's algebra of a bipartite model, where there is neither finite dimension nor, in general, a square root.

Neither is needed. In a star-ordered ring a nonnegative element is a finite sum ∑ Zᵢᴴ Zᵢ (exists_sum_star_mul_self), so each element of a POVM Q is ∑ᵢ Z_{a,i}ᴴ Z_{a,i}, and the whole POVM is the Kraus family (Z_{a,i})_{a,i} with ∑_{a,i} Z_{a,i}ᴴ Z_{a,i} = 1. The Halmos unitary of its Naimark matrix (MIPRE/Foundations/HalmosDilation.lean) dilates it to projections proj w (a, i), which form a projective measurement (Halmos.isPVMIn_proj); coarse-grained over i, they compress at the fixed basis vector e_{inl (a₀, 0)} to Q a (exists_pvm_dilation). The number of terms is padded to a common bound, so that one ancilla, DilationAncilla A K, serves a whole finite family of POVMs.

Finite sums of squares

theorem MIPRE.exists_sum_star_mul_self {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {x : R} (hx : 0 ≤ x) : ∃ (k : ℕ) (Z : Fin k → R), x = ∑ i : Fin k, star (Z i) * Z i

A nonnegative element of a star-ordered ring is a finite sum of squares Zᴴ Z.

theorem MIPRE.sum_star_mul_self_pad {R : Type u_1} [Ring R] [StarRing R] {k K : ℕ} (hk : k ≤ K) (Z : Fin k → R) : (∑ i : Fin K, star (if h : ↑i < k then Z ⟨↑i, h⟩ else 0) * if h : ↑i < k then Z ⟨↑i, h⟩ else 0) = ∑ i : Fin k, star (Z i) * Z i

A finite sum of squares, padded by zeros to any longer length.

The dilated projections form a projective measurement

theorem MIPRE.Halmos.coordProj_mul_coordProj {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] {a b : m} (hab : a ≠ b) : coordProj a * coordProj b = 0

theorem MIPRE.Halmos.isPVMIn_proj {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] {w : Matrix m m R} (hw : w * w.conjTranspose * w = w) : IsPVMIn (proj w)

The dilated projections of a partial isometry form a projective measurement.

Dilation of a family of POVMs against one fixed state

@[reducible, inline]

abbrev MIPRE.DilationAncilla (A : Type u_1) (K : ℕ) : Type u_1

The ancilla of the fixed-state dilation of POVMs with outcomes A, padded to K + 1 terms: two copies of A × Fin (K + 1).

Equations

• MIPRE.DilationAncilla A K = (A × Fin (K + 1) ⊕ A × Fin (K + 1))

theorem MIPRE.exists_pvm_dilation_ge {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {Y : Type u_2} {A : Type u_3} [Fintype Y] [Fintype A] [DecidableEq A] (Q : Y → POVMIn A R) (a₀ : A) : ∃ (K₀ : ℕ), ∀ (K : ℕ), K₀ ≤ K → ∃ (P : Y → A → Matrix (DilationAncilla A K) (DilationAncilla A K) R), (∀ (y : Y), IsPVMIn (P y)) ∧ ∀ (y : Y) (a : A), P y a (Sum.inl (a₀, 0)) (Sum.inl (a₀, 0)) = (Q y).op a

Fixed-state dilation with any large enough padding: the dilation of exists_pvm_dilation exists on DilationAncilla A K for every K beyond a threshold, so that finitely many families, even in different rings, can share one ancilla.

theorem MIPRE.exists_pvm_dilation {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {Y : Type u_2} {A : Type u_3} [Fintype Y] [Fintype A] [DecidableEq A] (Q : Y → POVMIn A R) (a₀ : A) : ∃ (K : ℕ) (P : Y → A → Matrix (DilationAncilla A K) (DilationAncilla A K) R), (∀ (y : Y), IsPVMIn (P y)) ∧ ∀ (y : Y) (a : A), P y a (Sum.inl (a₀, 0)) (Sum.inl (a₀, 0)) = (Q y).op a

Every finite family of POVMs in a star-ordered ring dilates to projective measurements against one fixed basis vector: projective P y on the ancilla DilationAncilla A K, whose (inl (a₀, 0), inl (a₀, 0)) entry is Q y.