Operator bounds relative to p

theorem Orthogonalization.MvN.one_sub_mul_proj_mul_one_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {p s : H →L[ℂ] H} (hsp : s * p = s) (hps : p * s = s) : (1 - s) * p * (1 - s) = p - s - s + s * s

(1 - s) p (1 - s) = p - s - s + s² when s is supported in p (s p = s = p s).

theorem Orthogonalization.MvN.proj_sub_two_mul_add_sq_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {p s : H →L[ℂ] H} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : p - s - s + s * s ≤ p - s * s

p - s - s + s² ≤ p - s² for 0 ≤ s ≤ 1: the difference is 2 (s - s²) ≥ 0.

The three-term estimate in the corner

theorem Orthogonalization.MvN.assembled_bound_rel {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {p : H →L[ℂ] H} (hp : IsStarProjection p) (hpM : p ∈ M) (hφp : φ p = 1) {ι : Type u_2} [Fintype ι] (a q p' : ι → H →L[ℂ] H) (s : H →L[ℂ] H) (haM : ∀ (i : ι), a i ∈ M) (ha0 : ∀ (i : ι), 0 ≤ a i) (hap : ∑ i : ι, a i = p) (hq : ∀ (i : ι), IsStarProjection (q i)) (hqM : ∀ (i : ι), q i ∈ M) (hqa : ∀ (i : ι), Commute (q i) (a i)) (hp' : ∀ (i : ι), IsStarProjection (p' i)) (hp'M : ∀ (i : ι), p' i ∈ M) (hp'sum : ∑ i : ι, p' i = p) (hsM : s ∈ M) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (hsp : s * p = s) (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 * ε

Step F3 relative to a projection. The three-term estimate of the paper in the corner p M p: the POVM (a_i) of M sums to the projection p ∈ M, the projections (p'_i) of M sum to p, the functional φ is positive on M with φ p = 1, and s ∈ M is an abstract square root of ∑ j, q_j a_j supported in p. Then φ (∑ i, |a_i - p'_i|²) < 9 ε whenever φ (∑ i, a_i²) > 1 - ε and φ (∑ i, q_i a_i) ≥ 1 - ε.

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, bounds ∑ b_i* b_i ≤ p - ∑ q_j a_j, ∑ d_i* d_i ≤ p - ∑ q_j a_j, ∑ c_i* c_i ≤ p - ∑ a_i² in M, evaluates φ, and assembles with the weighted triangle inequality (‖b + d‖² ≤ 2 ‖b‖² + 2 ‖d‖², then ‖(b + d) + c‖² ≤ (3/2) ‖b + d‖² + 3 ‖c‖²).