structure Orthogonalization.Blocks.IsCentralProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (z : H →L[ℂ] H) : Prop

A central projection of M: a projection belonging to M and commuting with every element of M.

• isStarProjection : IsStarProjection z
• mem : z ∈ M
• commute (x : H →L[ℂ] H) : x ∈ M → Commute z x

def Orthogonalization.Blocks.OrthAt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (z : H →L[ℂ] H) (ι : Type u_2) [Fintype ι] : Prop

Theorem 1.2 at z (proof-side): for every functional φ positive on M with φ z = 1 and every POVM (a i) in M supported in z (positive elements of M summing to z) with φ (∑ a i²) > 1 − ε, there is a PVM (p i) in M supported in z (projections of M with p i z = p i, summing to z) with φ (∑ |a i − p i|²) < 9 ε.

Equations

• One or more equations did not get rendered due to their size.

Elementary facts about operators supported in a projection

theorem Orthogonalization.Blocks.mul_eq_self_of_le_proj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {a z : H →L[ℂ] H} (hz : IsStarProjection z) (ha0 : 0 ≤ a) (haz : a ≤ z) : a * z = a

A positive operator dominated by a projection is supported in it: 0 ≤ a ≤ z with z a projection gives a z = a.

theorem Orthogonalization.Blocks.proj_mul_eq_self_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {p z : H →L[ℂ] H} (hp : IsStarProjection p) (hz : IsStarProjection z) (hpz : p ≤ z) : p * z = p

A projection p ≤ z (z a projection) satisfies p z = p.

theorem Orthogonalization.Blocks.proj_mul_left_of_mul_right {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {p z : H →L[ℂ] H} (hp : IsStarProjection p) (hz : IsStarProjection z) (h : p * z = p) : z * p = p

If p z = p for projections p, z, then also z p = p.

theorem Orthogonalization.Blocks.le_of_sum_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] {a : ι → H →L[ℂ] H} {z : H →L[ℂ] H} (ha0 : ∀ (i : ι), 0 ≤ a i) (haz : ∑ i : ι, a i = z) (i : ι) : a i ≤ z

Each term of a family of positive operators summing to z is dominated by z.

theorem Orthogonalization.Blocks.mul_eq_self_of_sum_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] {a : ι → H →L[ℂ] H} {z : H →L[ℂ] H} (hz : IsStarProjection z) (ha0 : ∀ (i : ι), 0 ≤ a i) (haz : ∑ i : ι, a i = z) (i : ι) : a i * z = a i

Each term of a family of positive operators summing to a projection z is supported in z.