Vector states

noncomputable def Orthogonalization.Corollaries.vecFunctional {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ξ : H) : (H →L[ℂ] H) →ₗ[ℂ] ℂ

The vector functional x ↦ ⟪ξ, x ξ⟫.

Equations

• Orthogonalization.Corollaries.vecFunctional ξ = { toFun := fun (x : H →L[ℂ] H) => inner ℂ ξ (x ξ), map_add' := ⋯, map_smul' := ⋯ }

theorem Orthogonalization.Corollaries.vecFunctional_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ξ : H) (x : H →L[ℂ] H) : (vecFunctional ξ) x = inner ℂ ξ (x ξ)

theorem Orthogonalization.Corollaries.vecFunctional_star_mul_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ξ : H) (b : H →L[ℂ] H) : (vecFunctional ξ) (star b * b) = ↑(‖b ξ‖ ^ 2)

⟪ξ, (b* b) ξ⟫ = ‖b ξ‖².

theorem Orthogonalization.Corollaries.re_vecFunctional_star_mul_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ξ : H) (b : H →L[ℂ] H) : ((vecFunctional ξ) (star b * b)).re = ‖b ξ‖ ^ 2

theorem Orthogonalization.Corollaries.vecFunctional_star_mul_self_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ξ : H) (b : H →L[ℂ] H) : 0 ≤ (vecFunctional ξ) (star b * b)

theorem Orthogonalization.Corollaries.vecFunctional_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ξ : H) (hξ : ‖ξ‖ = 1) : (vecFunctional ξ) 1 = 1

theorem Orthogonalization.Corollaries.re_vecFunctional_sum_mul_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] (ξ : H) (a : ι → H →L[ℂ] H) (ha : ∀ (i : ι), IsSelfAdjoint (a i)) : ((vecFunctional ξ) (∑ i : ι, a i * a i)).re = ∑ i : ι, ‖(a i) ξ‖ ^ 2

⟪ξ, (∑ a_i²) ξ⟫ = ∑ ‖a_i ξ‖² for self-adjoint a_i.

theorem Orthogonalization.Corollaries.re_vecFunctional_sum_star_sub_mul_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] (ξ : H) (a p : ι → H →L[ℂ] H) : ((vecFunctional ξ) (∑ i : ι, star (a i - p i) * (a i - p i))).re = ∑ i : ι, ‖(a i) ξ - (p i) ξ‖ ^ 2

⟪ξ, (∑ |a_i − p_i|²) ξ⟫ = ∑ ‖a_i ξ − p_i ξ‖².

noncomputable def Orthogonalization.Corollaries.vecState {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (ξ : H) (hξ : ‖ξ‖ = 1) : NormalState M

The vector state x ↦ ⟪ξ, x ξ⟫ of a unit vector ξ, as a normal state of any von Neumann algebra M (it is positive and normal on all of B(H)).

Equations

• Orthogonalization.Corollaries.vecState M ξ hξ = { toLinearMap := Orthogonalization.Corollaries.vecFunctional ξ, map_one' := ⋯, nonneg' := ⋯, normal' := ⋯ }

theorem Orthogonalization.Corollaries.vecState_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (ξ : H) (hξ : ‖ξ‖ = 1) (x : H →L[ℂ] H) : (vecState M ξ hξ).toLinearMap x = (vecFunctional ξ) x

Restriction of a normal state to a smaller von Neumann algebra

def Orthogonalization.Corollaries.restrictState {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M N : VonNeumannAlgebra H} (φ : NormalState M) (hNM : ∀ x ∈ N, x ∈ M) : NormalState N

A normal state of M is a normal state of every von Neumann subalgebra N ≤ M (same functional; DIFFERENCES.md D1).

Equations

• Orthogonalization.Corollaries.restrictState φ hNM = { toLinearMap := φ.toLinearMap, map_one' := ⋯, nonneg' := ⋯, normal' := ⋯ }

theorem Orthogonalization.Corollaries.restrictState_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M N : VonNeumannAlgebra H} (φ : NormalState M) (hNM : ∀ x ∈ N, x ∈ M) (x : H →L[ℂ] H) : (restrictState φ hNM).toLinearMap x = φ.toLinearMap x

The seminorm of a normal state

theorem Orthogonalization.Corollaries.normSq_nonneg_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} (φ : NormalState M) {x : H →L[ℂ] H} (hx : x ∈ M) : 0 ≤ φ.normSq x

‖x‖_φ² ≥ 0 for x ∈ M.

theorem Orthogonalization.Corollaries.le_two_mul_sqrt_mul_sqrt {A B D : ℝ} (hA : 0 ≤ A) (hD : 0 ≤ D) (h : ∀ (s t : ℝ), 0 ≤ s ^ 2 * A - s * t * B + t ^ 2 * D) : B ≤ 2 * (√A * √D)

Real arithmetic behind the discriminant argument: if 0 ≤ s² A − s t B + t² D for all real s, t, with A, D ≥ 0, then B ≤ 2 √A √D.

theorem Orthogonalization.Corollaries.re_add_re_le_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {x y : H →L[ℂ] H} (hx : x ∈ M) (hy : y ∈ M) : (φ (star x * y)).re + (φ (star y * x)).re ≤ 2 * (√(φ (star x * x)).re * √(φ (star y * y)).re)

Cauchy–Schwarz (real form) for a functional positive on M: for x, y ∈ M, Re φ(x* y) + Re φ(y* x) ≤ 2 ‖x‖_φ ‖y‖_φ.

theorem Orthogonalization.Corollaries.sum_re_add_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {ι : Type u_2} [Fintype ι] (b c : ι → H →L[ℂ] H) (hb : ∀ (i : ι), b i ∈ M) (hc : ∀ (i : ι), c i ∈ M) : ∑ i : ι, (φ (star (b i + c i) * (b i + c i))).re ≤ (√(∑ i : ι, (φ (star (b i) * b i)).re) + √(∑ i : ι, (φ (star (c i) * c i)).re)) ^ 2

Triangle inequality (squared form) for the seminorm of tuples, for a state positive on M only: if all b_i, c_i ∈ M, then ∑ ‖b_i + c_i‖_φ² ≤ (√(∑ ‖b_i‖_φ²) + √(∑ ‖c_i‖_φ²))².

theorem Orthogonalization.Corollaries.sum_normSq_add_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} (φ : NormalState M) {ι : Type u_2} [Fintype ι] (b c : ι → H →L[ℂ] H) (hb : ∀ (i : ι), b i ∈ M) (hc : ∀ (i : ι), c i ∈ M) : ∑ i : ι, φ.normSq (b i + c i) ≤ (√(∑ i : ι, φ.normSq (b i)) + √(∑ i : ι, φ.normSq (c i))) ^ 2

The triangle inequality in the form used for Theorem 1.4: ∑ ‖b_i + c_i‖_φ² ≤ (√(∑ ‖b_i‖_φ²) + √(∑ ‖c_i‖_φ²))² for b_i, c_i ∈ M.

PVMs: orthogonality and the compressed POVM a_i = ∑_j q_j p_i q_j

theorem Orthogonalization.Corollaries.mul_eq_zero_of_ne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {κ : Type u_3} [Fintype κ] {q : κ → H →L[ℂ] H} (hq : IsPVM M q) {j k : κ} (hjk : j ≠ k) : q j * q k = 0

The projections of a PVM are pairwise orthogonal: q_j q_k = 0 for j ≠ k.

noncomputable def Orthogonalization.Corollaries.compress {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} {κ : Type u_3} [Fintype κ] (p : ι → H →L[ℂ] H) (q : κ → H →L[ℂ] H) (i : ι) : H →L[ℂ] H

The compressed POVM a_i = ∑_j q_j p_i q_j of Section 5 of the paper.

Equations

• Orthogonalization.Corollaries.compress p q i = ∑ j : κ, q j * p i * q j

theorem Orthogonalization.Corollaries.compress_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] {p : ι → H →L[ℂ] H} {q : κ → H →L[ℂ] H} (hp : IsPVM M p) (hq : IsPVM M q) (i : ι) : compress p q i ∈ M

theorem Orthogonalization.Corollaries.compress_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] {p : ι → H →L[ℂ] H} {q : κ → H →L[ℂ] H} (hp : IsPVM M p) (hq : IsPVM M q) (i : ι) : star (compress p q i) = compress p q i

theorem Orthogonalization.Corollaries.compress_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] {p : ι → H →L[ℂ] H} {q : κ → H →L[ℂ] H} (hp : IsPVM M p) (hq : IsPVM M q) (i : ι) : 0 ≤ compress p q i

theorem Orthogonalization.Corollaries.sum_compress {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] {p : ι → H →L[ℂ] H} {q : κ → H →L[ℂ] H} (hp : IsPVM M p) (hq : IsPVM M q) : ∑ i : ι, compress p q i = 1

theorem Orthogonalization.Corollaries.isPOVM_compress {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] {p : ι → H →L[ℂ] H} {q : κ → H →L[ℂ] H} (hp : IsPVM M p) (hq : IsPVM M q) : IsPOVM M (compress p q)

theorem Orthogonalization.Corollaries.mul_compress {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {ι : Type u_2} {κ : Type u_3} [Fintype κ] {p : ι → H →L[ℂ] H} {q : κ → H →L[ℂ] H} (hq : IsPVM M q) (i : ι) (k : κ) : q k * compress p q i = q k * p i * q k

theorem Orthogonalization.Corollaries.compress_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {ι : Type u_2} {κ : Type u_3} [Fintype κ] {p : ι → H →L[ℂ] H} {q : κ → H →L[ℂ] H} (hq : IsPVM M q) (i : ι) (k : κ) : compress p q i * q k = q k * p i * q k

theorem Orthogonalization.Corollaries.compress_comm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {ι : Type u_2} {κ : Type u_3} [Fintype κ] {p : ι → H →L[ℂ] H} {q : κ → H →L[ℂ] H} (hq : IsPVM M q) (i : ι) (k : κ) : Commute (compress p q i) (q k)

a_i commutes with every q_k.

theorem Orthogonalization.Corollaries.sum_star_sub_mul_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] {p : ι → H →L[ℂ] H} {q : κ → H →L[ℂ] H} (hp : IsPVM M p) (hq : IsPVM M q) (i : ι) : ∑ j : κ, star (p i * q j - q j * p i) * (p i * q j - q j * p i) = compress p q i + p i - compress p q i * p i - p i * compress p q i

∑_j |p_i q_j − q_j p_i|² = a_i + p_i − a_i p_i − p_i a_i.

theorem Orthogonalization.Corollaries.star_sub_compress_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] {p : ι → H →L[ℂ] H} {q : κ → H →L[ℂ] H} (hp : IsPVM M p) (hq : IsPVM M q) (i : ι) : star (p i - compress p q i) * (p i - compress p q i) = p i - p i * compress p q i - compress p q i * p i + compress p q i * compress p q i

|p_i − a_i|² = p_i − p_i a_i − a_i p_i + a_i².

theorem Orthogonalization.Corollaries.key_identity {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] {p : ι → H →L[ℂ] H} {q : κ → H →L[ℂ] H} (hp : IsPVM M p) (hq : IsPVM M q) : ∑ i : ι, ∑ j : κ, star (p i * q j - q j * p i) * (p i * q j - q j * p i) = ∑ i : ι, star (p i - compress p q i) * (p i - compress p q i) + (1 - ∑ i : ι, compress p q i * compress p q i)

The operator identity behind the display of Section 5: ∑_{i,j} |p_i q_j − q_j p_i|² = ∑_i |p_i − a_i|² + (1 − ∑_i a_i²).

theorem Orthogonalization.povm_orthogonalization_hilbert_finDim {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {ι : Type u_2} [Fintype ι] (a : ι → H →L[ℂ] H) (ha : (∀ (i : ι), (a i).IsPositive) ∧ ∑ i : ι, a i = 1) (ξ : H) (hξ : ‖ξ‖ = 1) (ε : ℝ) (hε : ε ∈ Set.Icc 0 1) (h : 1 - ε < ∑ i : ι, ‖(a i) ξ‖ ^ 2) : ∃ (p : ι → H →L[ℂ] H), (∀ (i : ι), IsStarProjection (p i)) ∧ ∑ i : ι, p i = 1 ∧ ∑ i : ι, ‖(a i) ξ - (p i) ξ‖ ^ 2 < 9 * ε ∧ ∀ (b : H →L[ℂ] H), (∀ (i : ι), Commute b (a i)) → ∀ (i : ι) (v : H), (p i) v = v → (p i) (b v) = b v

Theorem 1.1 (thm:orthonormalization_Hilbert) in finite dimension, with the commutant clause: the instance of the signed statement povm_orthogonalization_hilbert with [FiniteDimensional ℂ H] added. Proof: Theorem 1.2 in the von Neumann algebra W*(a_i) with the vector state x ↦ ⟪ξ, x ξ⟫; the projections lie in W*(a_i), so they commute with every b commuting with the a_i (bicommutant).

theorem Orthogonalization.pvm_almost_commute_finDim {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) (φ : NormalState M) {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] (p : ι → H →L[ℂ] H) (q : κ → H →L[ℂ] H) (hp : IsPVM M p) (hq : IsPVM M q) (ε : ℝ) (h : ∑ i : ι, ∑ j : κ, φ.normSq (p i * q j - q j * p i) < ε) : ∃ (p' : ι → H →L[ℂ] H), IsPVM M p' ∧ (∀ (i : ι) (j : κ), Commute (p' i) (q j)) ∧ ∑ i : ι, φ.normSq (p i - p' i) < 10 * ε

Theorem 1.4 (thm:pvm_almost_commute) in finite dimension: the instance of the signed statement pvm_almost_commute with [FiniteDimensional ℂ H] added. Proof (Section 5 of the paper): with a_i = ∑_j q_j p_i q_j, ∑_{i,j} ‖p_i q_j − q_j p_i‖_φ² = ∑_i ‖p_i − a_i‖_φ² + (1 − φ(∑ a_i²)); Theorem 1.2 in W*(a_i) (whose elements commute with the q_j) gives a PVM p' with ∑ ‖a_i − p'_i‖_φ² < 9 (ε − ∑ ‖p_i − a_i‖_φ²), and the triangle inequality together with (√D + √E)² ≤ 10 (D + E/9) concludes.