noncomputable def Orthogonalization.fullAlgebra (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : VonNeumannAlgebra H

The von Neumann algebra B(H) of all bounded operators on H.

Equations

• Orthogonalization.fullAlgebra H = { toStarSubalgebra := ⊤, centralizer_centralizer' := ⋯ }

@[simp]

theorem Orthogonalization.mem_fullAlgebra {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) : x ∈ fullAlgebra H

theorem Orthogonalization.povm_orthogonalization_finDim {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {ι : Type u_2} [Fintype ι] (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hφ : ∀ (x : H →L[ℂ] H), 0 ≤ φ (star x * x)) (hφ1 : φ 1 = 1) (a : ι → H →L[ℂ] H) (ha0 : ∀ (i : ι), 0 ≤ a i) (ha1 : ∑ i : ι, a i = 1) (ε : ℝ) (hε : 1 - ε < (φ (∑ i : ι, a i * a i)).re) : ∃ (p : ι → H →L[ℂ] H), (∀ (i : ι), IsStarProjection (p i)) ∧ ∑ i : ι, p i = 1 ∧ (φ (∑ i : ι, star (a i - p i) * (a i - p i))).re < 9 * ε

Theorem 1.2 for B(H), H finite-dimensional, any state. A POVM (a i) on a finite-dimensional Hilbert space and a positive normalized linear functional φ on B(H) with φ(∑ a i²) > 1 − ε admit a PVM (p i) on H with φ(∑ |a i − p i|²) < 9ε.

theorem Orthogonalization.povm_orthogonalization_of_mem_all {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {ι : Type u_2} [Fintype ι] (M : VonNeumannAlgebra H) (hM : ∀ (x : H →L[ℂ] H), x ∈ M) (φ : NormalState M) (a : ι → H →L[ℂ] H) (ha : IsPOVM M a) (ε : ℝ) (hε : 1 - ε < (φ.toLinearMap (∑ i : ι, a i * a i)).re) : ∃ (p : ι → H →L[ℂ] H), IsPVM M p ∧ (φ.toLinearMap (∑ i : ι, star (a i - p i) * (a i - p i))).re < 9 * ε

Theorem 1.2 (povm_orthogonalization) for a von Neumann algebra M containing every operator of the finite-dimensional space H: the instance of the signed statement delivered by tier T1a.

theorem Orthogonalization.povm_orthogonalization_fullAlgebra {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {ι : Type u_2} [Fintype ι] (φ : NormalState (fullAlgebra H)) (a : ι → H →L[ℂ] H) (ha : IsPOVM (fullAlgebra H) a) (ε : ℝ) (hε : 1 - ε < (φ.toLinearMap (∑ i : ι, a i * a i)).re) : ∃ (p : ι → H →L[ℂ] H), IsPVM (fullAlgebra H) p ∧ (φ.toLinearMap (∑ i : ι, star (a i - p i) * (a i - p i))).re < 9 * ε

Theorem 1.2 (povm_orthogonalization) for M = B(H), H finite-dimensional.