Naimark dilation against a fixed state

A POVM is the compression of a projective measurement on a larger space. What the applications need is more than that: a whole question-indexed family of POVMs must be the compression of a family of projective measurements by one question-independent isometry, because the state the expectations are taken against is shared and must not depend on the question. exists_projective_dilation is that statement, and the unitary extension (exists_unitary_extending) is the step that buys it.

This file was extracted from MIPRE/Background/Repetition/Entangled.lean, where it was written for the dilation direction of lem:povm-value-eq. It is generic mathematics --- matrices, an ancilla register, and the completion of an orthonormal family to a basis --- and it reaches none of the vendored trees, but Entangled.lean imports the 71k-line vendored Repetition/TenProofs/QuantumParallelRepetition, and MIPRE/LCS/ may not import MIPRE/Background/ at all. The second consumer is blueprint lem:ms-direct-anticomm, whose proof dilates each of the Magic Square's six constraint POVMs against one shared ancilla, so the code has to live outside MIPRE/Background/ to be usable at all.

The Born-rule transport lemmas at the end travel with it: they are how a dilated projective measurement is compressed back, and they say nothing about repetition either.

Naimark dilation of a question-indexed family

The second input to the dilation direction. A POVM dilates to an isometry into one extra register (exists_isometry_of_povm); extending that isometry to a unitary turns it into a projective measurement on the larger space whose expectations against a fixed state are the POVM's. The extension is what makes the construction work for a whole question-indexed family at once: the isometry depends on the question, the state must not.

def MIPRE.ancillaProj (d : Type u_1) [DecidableEq d] {A : Type u_2} [DecidableEq A] (a : A) : Matrix (d × A) (d × A) ℂ

The ancilla projection 1 ⊗ |a⟩⟨a| on d × A: the identity on the first factor and the rank-one projection onto a on the second. It is a diagonal matrix, and saying so is what makes the dilation computations below elementary.

Equations

• MIPRE.ancillaProj d a = Matrix.diagonal fun (p : d × A) => if p.2 = a then 1 else 0

theorem MIPRE.ancillaProj_conjTranspose {d : Type u_1} {A : Type u_2} [DecidableEq d] [DecidableEq A] (a : A) : (ancillaProj d a).conjTranspose = ancillaProj d a

theorem MIPRE.ancillaProj_mul_self {d : Type u_1} {A : Type u_2} [Fintype d] [DecidableEq d] [Fintype A] [DecidableEq A] (a : A) : ancillaProj d a * ancillaProj d a = ancillaProj d a

theorem MIPRE.sum_ancillaProj {d : Type u_1} {A : Type u_2} [DecidableEq d] [Fintype A] [DecidableEq A] : ∑ a : A, ancillaProj d a = 1

theorem MIPRE.exists_isometry_of_povm {d : Type u_1} {A : Type u_2} [Fintype d] [DecidableEq d] [Fintype A] [DecidableEq A] {E : A → Matrix d d ℂ} (hpos : ∀ (a : A), (E a).PosSemidef) (hsum : ∑ a : A, E a = 1) : ∃ (V : Matrix (d × A) d ℂ), V.conjTranspose * V = 1 ∧ ∀ (a : A), V.conjTranspose * (ancillaProj d a * V) = E a

Every POVM dilates to an isometry into one extra register: there is V with Vᴴ V = 1 and Vᴴ (1 ⊗ |a⟩⟨a|) V = E a. Only the factorization of a positive semidefinite matrix is used, not a square root: with E a = (K a)ᴴ (K a), the isometry is V : v ↦ ∑ a, (K a v) ⊗ |a⟩.

def MIPRE.ancillaEmbed (d : Type u_1) [DecidableEq d] {A : Type u_2} [DecidableEq A] (a₀ : A) : Matrix (d × A) d ℂ

The isometry d → d × A that pads a vector with the fixed ancilla state |a₀⟩.

Equations

• MIPRE.ancillaEmbed d a₀ = Matrix.of fun (p : d × A) (j : d) => if p = (j, a₀) then 1 else 0

theorem MIPRE.ancillaEmbed_isometry {d : Type u_1} {A : Type u_2} [Fintype d] [DecidableEq d] [Fintype A] [DecidableEq A] (a₀ : A) : (ancillaEmbed d a₀).conjTranspose * ancillaEmbed d a₀ = 1

theorem MIPRE.exists_unitary_extending {d : Type u_1} {A : Type u_2} [Fintype d] [DecidableEq d] [Fintype A] [DecidableEq A] (a₀ : A) {V : Matrix (d × A) d ℂ} (hV : V.conjTranspose * V = 1) : ∃ (U : Matrix (d × A) (d × A) ℂ), U.conjTranspose * U = 1 ∧ U * ancillaEmbed d a₀ = V

Any isometry into d × A extends to a unitary of d × A agreeing with it on the a₀-slice: U · (ancillaEmbed d a₀) = V. This is the completion of an orthonormal family to an orthonormal basis, imported from Mathlib as Orthonormal.exists_orthonormalBasis_extension_of_card_eq; it is the step that lets a whole question-indexed family of POVMs be dilated against one fixed state.

theorem MIPRE.exists_projective_dilation {d : Type u_1} {A : Type u_2} {X : Type u_3} [Fintype d] [DecidableEq d] [Fintype A] [DecidableEq A] (a₀ : A) {E : X → A → Matrix d d ℂ} (hpos : ∀ (x : X) (a : A), (E x a).PosSemidef) (hsum : ∀ (x : X), ∑ a : A, E x a = 1) : ∃ (P : X → A → Matrix (d × A) (d × A) ℂ), (∀ (x : X) (a : A), star (P x a) = P x a) ∧ (∀ (x : X) (a : A), P x a * P x a = P x a) ∧ (∀ (x : X), ∑ a : A, P x a = 1) ∧ ∀ (x : X) (a : A), (ancillaEmbed d a₀).conjTranspose * (P x a * ancillaEmbed d a₀) = E x a

Naimark dilation of a question-indexed POVM family against a fixed state. A family of POVMs {E^x_a} on d is the compression, by the single question-independent isometry ancillaEmbed d a₀, of a family of genuinely projective measurements {P^x_a} on d × A. That the compression does not depend on the question is what lets the dilation be applied to a fixed shared state, and it is why the unitary extension of the previous step was needed.

Transport of Born-rule expectations

Three ways a quadratic form ⟨v| M |v⟩ moves: along a bijective reindexing of the space, along an arbitrary linear map (which is how a dilation is compressed back), and the special case M = 1 that transports unit vectors.

theorem MIPRE.dotProduct_mulVec_submatrix {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (M : Matrix κ κ ℂ) (v : κ → ℂ) : star (v ∘ ⇑e) ⬝ᵥ (M.submatrix ⇑e ⇑e).mulVec (v ∘ ⇑e) = star v ⬝ᵥ M.mulVec v

Reindexing the space by a bijection changes no Born-rule expectation.

theorem MIPRE.dotProduct_comp_equiv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (v : κ → ℂ) : star (v ∘ ⇑e) ⬝ᵥ v ∘ ⇑e = star v ⬝ᵥ v

Reindexing the space by a bijection preserves the norm.

theorem MIPRE.dotProduct_mulVec_conj {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (W : Matrix κ ι ℂ) (M : Matrix κ κ ℂ) (v : ι → ℂ) : star (W.mulVec v) ⬝ᵥ M.mulVec (W.mulVec v) = star v ⬝ᵥ (W.conjTranspose * (M * W)).mulVec v

Pulling a Born-rule expectation back along a linear map W conjugates the observable: ⟨Wv| M |Wv⟩ = ⟨v| Wᴴ M W |v⟩. With W an isometry and M a projection this is how a dilated projective measurement compresses back to the POVM it came from.