The assembled projections

noncomputable def Orthogonalization.assembledPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} (w : ι → H →L[ℂ] H) (i : ι) : H →L[ℂ] H

The PVM assembled from the isometry data: p_i = w_i* w_i, which is the paper's p_i = u* t_i u for t_i = e_{ii} ⊗ q_i read block by block.

Equations

• Orthogonalization.assembledPVM w i = star (w i) * w i

theorem Orthogonalization.IsometryData.q_mul_w {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {a q w : ι → H →L[ℂ] H} (hw : IsometryData a q w) (i : ι) : q i * w i = w i

From (W1) and (W2): q_i w_i = w_i. Indeed q_i w_i = ∑ j, (w_i w_j*) w_j = w_i ∑ j, w_j* w_j = w_i.

theorem Orthogonalization.assembledPVM_isStarProjection {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {a q w : ι → H →L[ℂ] H} (hw : IsometryData a q w) (i : ι) : IsStarProjection (assembledPVM w i)

Each p_i = w_i* w_i is a star projection: self-adjointness is star_mul/star_star, and idempotence follows from (W2) and IsometryData.q_mul_w, since (w_i* w_i)(w_i* w_i) = w_i* (w_i w_i*) w_i = w_i* q_i w_i = w_i* w_i.

theorem Orthogonalization.sum_assembledPVM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {a q w : ι → H →L[ℂ] H} (hw : IsometryData a q w) : ∑ i : ι, assembledPVM w i = 1

The assembled projections sum to 1: this is (W1).

theorem Orthogonalization.sqrt_mul_assembledPVM_mul_sqrt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {a q w : ι → H →L[ℂ] H} (hw : IsometryData a q w) (hq : ∀ (i : ι), IsStarProjection (q i)) (hqa : ∀ (i : ι), Commute (q i) (a i)) (ha0 : ∀ (i : ι), 0 ≤ a i) (i : ι) : CFC.sqrt (∑ j : ι, q j * a j) * assembledPVM w i * CFC.sqrt (∑ j : ι, q j * a j) = q i * a i

The paper's identity |x| p_i |x| = q_i a_i (with |x| = √(∑ j, q_j a_j)): s p_i s = (w_i s)* (w_i s) = (q_i √a_i)* (q_i √a_i) = √a_i q_i √a_i = q_i a_i, using (W3), self-adjointness of s and of √a_i, idempotence of q_i, and the fact that q_i commutes with √a_i.

Operator identities and inequalities for the three terms

theorem Orthogonalization.IsStarProjection.mul_le_mul_of_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {r : H →L[ℂ] H} (hr : IsStarProjection r) {u v : H →L[ℂ] H} (huv : u ≤ v) (h : Commute r (v - u)) : r * u ≤ r * v

Monotonicity of the compression by a projection commuting with the difference: if u ≤ v, r is a projection and r commutes with v - u, then r u ≤ r v, because r (v - u) is a product of commuting positive operators.

theorem Orthogonalization.star_mul_self_proj_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {r x : H →L[ℂ] H} (hr : IsStarProjection r) (hx : IsSelfAdjoint x) (h : Commute r x) : star (r * x) * (r * x) = r * (x * x)

(r x)* (r x) = r x² for a projection r commuting with a self-adjoint x. This is the first term of the paper's decomposition, with r = 1 - q_i.

theorem Orthogonalization.star_mul_self_proj_mul_sub_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s p : H →L[ℂ] H} (hp : IsStarProjection p) (hs : star s = s) : star (p * s - p) * (p * s - p) = (1 - s) * p * (1 - s)

(p (s - 1))* (p (s - 1)) = (1 - s) p (1 - s) for a projection p and a self-adjoint s. This is the third term of the paper's decomposition.

theorem Orthogonalization.star_mul_self_sub_one_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : H →L[ℂ] H} (hs : star s = s) (x : H →L[ℂ] H) : star ((s - 1) * x) * ((s - 1) * x) = star x * ((1 - s) * (1 - s)) * x

((s - 1) x)* ((s - 1) x) = x* (1 - s)² x for a self-adjoint s; the conjugating element of the second term of the paper's decomposition.

theorem Orthogonalization.conj_one_sub_sq_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {s z p : H →L[ℂ] H} (hp : p * p = p) (hps : s * p * s = z) : s * p * (1 - s * s) * (p * s) = z - z * z

With s p s = z and p idempotent: s p (1 - s²) p s = z - z². This is the paper's |x| p_i (1 - |x|²) p_i |x| = |x| p_i |x| - (|x| p_i |x|)².

theorem Orthogonalization.proj_mul_sub_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x qq : H →L[ℂ] H} (hq : IsStarProjection qq) (h : Commute qq x) : qq * x - qq * x * (qq * x) = qq * (x - x * x)

q x - (q x)² = q (x - x²) for a projection q commuting with x.

The φ-step

theorem Orthogonalization.phiNormSq_le_re_map_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) {ι : Type u_2} [Fintype ι] {b : ι → H →L[ℂ] H} {x : H →L[ℂ] H} (h : ∑ i : ι, star (b i) * b i ≤ x) : phiNormSq φ b ≤ (φ x).re

If the operator ∑ i, b_i* b_i is dominated by x, then the squared seminorm ‖(b_i)‖_φ² is dominated by φ x (real parts): the real part of a positive functional is monotone.

The three-term estimate

theorem Orthogonalization.assembled_bound_core {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hφ : ∀ (x : H →L[ℂ] H), 0 ≤ φ (star x * x)) (hφ1 : φ 1 = 1) (a q p : ι → H →L[ℂ] H) (s : H →L[ℂ] H) (ha0 : ∀ (i : ι), 0 ≤ a i) (ha1 : ∑ i : ι, a i = 1) (hq : ∀ (i : ι), IsStarProjection (q i)) (hqa : ∀ (i : ι), Commute (q i) (a i)) (hp : ∀ (i : ι), IsStarProjection (p i)) (hpsum : ∑ i : ι, p i = 1) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (hss : s * s = ∑ j : ι, q j * a j) (hsp : ∀ (i : ι), s * p i * s = q i * a i) (ε : ℝ) (hε : 1 - ε < (φ (∑ i : ι, a i * a i)).re) (hlarge : 1 - ε ≤ (φ (∑ i : ι, q i * a i)).re) : (φ (∑ i : ι, star (a i - p i) * (a i - p i))).re < 9 * ε

The core of step F3. The paper's estimate, with the square root |x| = √(∑ j, q_j a_j) abstracted into an operator s subject only to the properties the argument uses: 0 ≤ s ≤ 1, s² = ∑ j, q_j a_j and s p_i s = q_i a_i.

The proof decomposes a_i - p_i = b_i + d_i + c_i with b_i = (1 - q_i) a_i, d_i = p_i s - p_i, c_i = q_i a_i - p_i s and bounds ‖b‖_φ² ≤ ε, ‖d‖_φ² ≤ ε, ‖c‖_φ² < ε; three applications of the triangle inequality (phiNormSq_add_add_lt) then give the constant 9.

theorem Orthogonalization.assembled_bound {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hφ : ∀ (x : H →L[ℂ] H), 0 ≤ φ (star x * x)) (hφ1 : φ 1 = 1) (a q w : ι → H →L[ℂ] H) (ha0 : ∀ (i : ι), 0 ≤ a i) (ha1 : ∑ i : ι, a i = 1) (hq : ∀ (i : ι), IsStarProjection (q i)) (hqa : ∀ (i : ι), Commute (q i) (a i)) (hw : IsometryData a q w) (ε : ℝ) (hε : 1 - ε < (φ (∑ i : ι, a i * a i)).re) (hlarge : 1 - ε ≤ (φ (∑ i : ι, q i * a i)).re) : (φ (∑ i : ι, star (a i - assembledPVM w i) * (a i - assembledPVM w i))).re < 9 * ε

Step F3 of the proof of Theorem 1.2 in the finite case. Given the isometry data (w_i) of Lemma 3.2 for a POVM (a_i) and the commuting projections (q_i) of Lemma 3.1, the assembled PVM p_i = w_i* w_i satisfies φ (∑ i, |a_i - p_i|²) < 9 ε whenever φ (∑ i, a_i²) > 1 - ε and φ (∑ i, q_i a_i) ≥ 1 - ε.