The Halmos unitary of a partial isometry, and the dilation of a positive operator valued measure

Plain algebra in the ring of matrices over a star ring R, which MIPRE/Foundations/CommutingDilation.lean reads with R the bounded operators on a Hilbert space through MIPRE/Foundations/OperatorMatrix.lean.

• The Halmos unitary (Halmos.extension). For a partial isometry w (w wᴴ w = w) in Matrix m m R, the block matrix [[w, 1 − w wᴴ], [1 − wᴴ w, wᴴ]] on m ⊕ m is unitary (conjTranspose_mul_extension, extension_mul_conjTranspose). It extends w without comparing the two defect projections 1 − w wᴴ and 1 − wᴴ w; an extension of w inside Matrix m m R itself would have to compare them, and in infinite dimension, inside the commutant of another family of operators, that comparison is Murray–von Neumann theory.
• The Naimark matrix (Halmos.naimark). For a Kraus family s : m → R, ∑ a, s aᴴ s a = 1, the matrix whose a₀-th column is s and whose other columns vanish is a partial isometry, with wᴴ w the matrix unit at (a₀, a₀) (conjTranspose_naimark_mul_naimark', naimark_mul_conjTranspose_mul'); with self-adjoint entries, ∑ a, s a * s a = 1 (conjTranspose_naimark_mul_naimark, naimark_mul_conjTranspose_mul).
• The dilated projections (Halmos.proj). proj w a := Uᴴ Q_a U, with U the Halmos unitary and Q_a the diagonal projection onto the two copies of the coordinate a, is a star projection (isStarProjection_proj), the proj w a sum to one (sum_proj), the (inl a₀, inl a₀) entry of proj (naimark s a₀) a is s aᴴ s a (proj_naimark_inl_inl'), and proj (naimark s a₀) a commutes with the constant diagonal matrix of any c commuting with every s a (commute_diagonal_proj_naimark).

So a ↦ proj (naimark s a₀) a is a projection-valued measure that compresses, at the unit vector e_{inl a₀}, to the positive operator valued measure a ↦ s a * s a, and it commutes with whatever commutes with the s a. With s a = √E_a this is the commutation-preserving Naimark dilation of planning/mipco-track.md §5, Phase 1(a), and of reports/co-generalization-audit.md §4.

The Halmos unitary

def MIPRE.Halmos.extension {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] (w : Matrix m m R) : Matrix (m ⊕ m) (m ⊕ m) R

The Halmos extension of w: the block matrix [[w, 1 − w wᴴ], [1 − wᴴ w, wᴴ]].

Equations

• MIPRE.Halmos.extension w = Matrix.fromBlocks w (1 - w * w.conjTranspose) (1 - w.conjTranspose * w) w.conjTranspose

theorem MIPRE.Halmos.conjTranspose_extension {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] (w : Matrix m m R) : (extension w).conjTranspose = Matrix.fromBlocks w.conjTranspose (1 - w.conjTranspose * w) (1 - w * w.conjTranspose) w

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

theorem MIPRE.Halmos.mul_sub_conjTranspose_mul {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) : w * (1 - w.conjTranspose * w) = 0

theorem MIPRE.Halmos.sub_mul_conjTranspose_mul {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) : (1 - w * w.conjTranspose) * w = 0

theorem MIPRE.Halmos.conjTranspose_mul_sub {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) : w.conjTranspose * (1 - w * w.conjTranspose) = 0

theorem MIPRE.Halmos.sub_mul_conjTranspose {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) : (1 - w.conjTranspose * w) * w.conjTranspose = 0

theorem MIPRE.Halmos.sub_conjTranspose_mul_idem {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) : (1 - w.conjTranspose * w) * (1 - w.conjTranspose * w) = 1 - w.conjTranspose * w

theorem MIPRE.Halmos.sub_mul_conjTranspose_idem {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) : (1 - w * w.conjTranspose) * (1 - w * w.conjTranspose) = 1 - w * w.conjTranspose

theorem MIPRE.Halmos.conjTranspose_mul_extension {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) : (extension w).conjTranspose * extension w = 1

The Halmos extension of a partial isometry is an isometry.

theorem MIPRE.Halmos.extension_mul_conjTranspose {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) : extension w * (extension w).conjTranspose = 1

The Halmos extension of a partial isometry is a co-isometry.

The dilated projections

def MIPRE.Halmos.coordProj {m : Type u_1} [DecidableEq m] {R : Type u_2} [Ring R] (a : m) : Matrix (m ⊕ m) (m ⊕ m) R

The diagonal projection of R^(m ⊕ m) onto the two copies of the coordinate a.

Equations

• MIPRE.Halmos.coordProj a = Matrix.diagonal fun (k : m ⊕ m) => if Sum.elim id id k = a then 1 else 0

theorem MIPRE.Halmos.conjTranspose_coordProj {m : Type u_1} [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] (a : m) : (coordProj a).conjTranspose = coordProj a

theorem MIPRE.Halmos.coordProj_mul_self {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] (a : m) : coordProj a * coordProj a = coordProj a

theorem MIPRE.Halmos.sum_coordProj {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] : ∑ a : m, coordProj a = 1

def MIPRE.Halmos.proj {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] (w : Matrix m m R) (a : m) : Matrix (m ⊕ m) (m ⊕ m) R

The dilated projection at the outcome a: Uᴴ Q_a U, for U the Halmos extension.

Equations

• MIPRE.Halmos.proj w a = (MIPRE.Halmos.extension w).conjTranspose * MIPRE.Halmos.coordProj a * MIPRE.Halmos.extension w

theorem MIPRE.Halmos.isStarProjection_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) (a : m) : IsStarProjection (proj w a)

The dilated projections are star projections.

theorem MIPRE.Halmos.sum_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) : ∑ a : m, proj w a = 1

The dilated projections sum to one.

The Naimark matrix

def MIPRE.Halmos.naimark {m : Type u_1} [DecidableEq m] {R : Type u_2} [Ring R] (s : m → R) (a₀ : m) : Matrix m m R

The Naimark matrix of s at a₀: its a₀-th column is s, its other columns vanish.

Equations

• MIPRE.Halmos.naimark s a₀ = Matrix.of fun (i j : m) => if j = a₀ then s i else 0

A Kraus family

The column s need not be self-adjoint: ∑ a, s aᴴ s a = 1 is what makes the Naimark matrix a partial isometry, and the dilation then compresses to s aᴴ s a. The self-adjoint case below is this one with s aᴴ = s a.

theorem MIPRE.Halmos.conjTranspose_naimark_apply' {m : Type u_1} [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] (s : m → R) (a₀ i j : m) : (naimark s a₀).conjTranspose i j = if i = a₀ then star (s j) else 0

theorem MIPRE.Halmos.conjTranspose_naimark_mul_naimark' {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] {s : m → R} (hsum : ∑ a : m, star (s a) * s a = 1) (a₀ : m) : (naimark s a₀).conjTranspose * naimark s a₀ = Matrix.diagonal fun (j : m) => if j = a₀ then 1 else 0

wᴴ w is the matrix unit at (a₀, a₀).

theorem MIPRE.Halmos.naimark_mul_conjTranspose_mul' {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] {s : m → R} (hsum : ∑ a : m, star (s a) * s a = 1) (a₀ : m) : naimark s a₀ * (naimark s a₀).conjTranspose * naimark s a₀ = naimark s a₀

The Naimark matrix of a Kraus family is a partial isometry.

theorem MIPRE.Halmos.proj_naimark_inl_inl' {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] {s : m → R} (hsum : ∑ a : m, star (s a) * s a = 1) (a₀ a : m) : proj (naimark s a₀) a (Sum.inl a₀) (Sum.inl a₀) = star (s a) * s a

The dilation compresses to s aᴴ s a at e_{inl a₀}.

theorem MIPRE.Halmos.conjTranspose_naimark_apply {m : Type u_1} [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] {s : m → R} (hs : ∀ (a : m), star (s a) = s a) (a₀ i j : m) : (naimark s a₀).conjTranspose i j = if i = a₀ then s j else 0

theorem MIPRE.Halmos.sum_star_mul_self_of_selfAdjoint {m : Type u_1} [Fintype m] {R : Type u_2} [Ring R] [StarRing R] {s : m → R} (hs : ∀ (a : m), star (s a) = s a) (hsum : ∑ a : m, s a * s a = 1) : ∑ a : m, star (s a) * s a = 1

theorem MIPRE.Halmos.conjTranspose_naimark_mul_naimark {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] {s : m → R} (hs : ∀ (a : m), star (s a) = s a) (hsum : ∑ a : m, s a * s a = 1) (a₀ : m) : (naimark s a₀).conjTranspose * naimark s a₀ = Matrix.diagonal fun (j : m) => if j = a₀ then 1 else 0

wᴴ w is the matrix unit at (a₀, a₀).

theorem MIPRE.Halmos.naimark_mul_conjTranspose_mul {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] {s : m → R} (hs : ∀ (a : m), star (s a) = s a) (hsum : ∑ a : m, s a * s a = 1) (a₀ : m) : naimark s a₀ * (naimark s a₀).conjTranspose * naimark s a₀ = naimark s a₀

The Naimark matrix is a partial isometry.

theorem MIPRE.Halmos.proj_naimark_inl_inl {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] {s : m → R} (hs : ∀ (a : m), star (s a) = s a) (hsum : ∑ a : m, s a * s a = 1) (a₀ a : m) : proj (naimark s a₀) a (Sum.inl a₀) (Sum.inl a₀) = s a * s a

The dilation compresses to s a * s a at e_{inl a₀}.

theorem MIPRE.Halmos.commute_diagonal_naimark {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] {s : m → R} {c : R} (hc : ∀ (a : m), Commute c (s a)) (a₀ : m) : Commute (Matrix.diagonal fun (x : m) => c) (naimark s a₀)

theorem MIPRE.Halmos.commute_diagonal_conjTranspose_naimark {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] {s : m → R} (hs : ∀ (a : m), star (s a) = s a) {c : R} (hc : ∀ (a : m), Commute c (s a)) (a₀ : m) : Commute (Matrix.diagonal fun (x : m) => c) (naimark s a₀).conjTranspose

theorem MIPRE.Halmos.commute_fromBlocks_diagonal {m : Type u_1} [Fintype m] {R : Type u_2} [Ring R] {D X Y Z W : Matrix m m R} (hX : Commute D X) (hY : Commute D Y) (hZ : Commute D Z) (hW : Commute D W) : Commute (Matrix.fromBlocks D 0 0 D) (Matrix.fromBlocks X Y Z W)

theorem MIPRE.Halmos.diagonal_const_eq_fromBlocks {m : Type u_1} [DecidableEq m] {R : Type u_2} [Ring R] (c : R) : (Matrix.diagonal fun (x : m ⊕ m) => c) = Matrix.fromBlocks (Matrix.diagonal fun (x : m) => c) 0 0 (Matrix.diagonal fun (x : m) => c)

theorem MIPRE.Halmos.commute_diagonal_proj_naimark {m : Type u_1} [Fintype m] [DecidableEq m] {R : Type u_2} [Ring R] [StarRing R] {s : m → R} (hs : ∀ (a : m), star (s a) = s a) {c : R} (hc : ∀ (a : m), Commute c (s a)) (a₀ a : m) : Commute (Matrix.diagonal fun (x : m ⊕ m) => c) (proj (naimark s a₀) a)

The dilation commutes with whatever commutes with the s a.