def Orthogonalization.IsPOVM {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {ι : Type u_1} [Fintype ι] (a : ι → H →L[ℂ] H) : Prop

A POVM in M with output set ι: a finite family of positive operators of M summing to 1 ("partition of unity" / "POVM", Section 1).

Equations

• Orthogonalization.IsPOVM M a = ((∀ (i : ι), a i ∈ M) ∧ (∀ (i : ι), (a i).IsPositive) ∧ ∑ i : ι, a i = 1)

def Orthogonalization.IsPVM {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {ι : Type u_1} [Fintype ι] (p : ι → H →L[ℂ] H) : Prop

A PVM in M: a family of projections of M summing to 1 ("PVM if in addition all the t_i's are projections", Section 1; pairwise orthogonality follows and is not part of the definition).

Equations

• Orthogonalization.IsPVM M p = ((∀ (i : ι), p i ∈ M) ∧ (∀ (i : ι), IsStarProjection (p i)) ∧ ∑ i : ι, p i = 1)

structure Orthogonalization.NormalState {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) : Type u

A normal state on the von Neumann algebra M (Section 2: "a linear map φ : M → ℂ that is positive (φ(x*x) ≥ 0 for every x ∈ M), normalized by φ(1) = 1 and weak-* continuous"). Weak-* continuity of a positive functional is rendered, as in the sister project, by continuity along bounded strongly convergent nets of elements of M (CommutingRepetition.VN.TendstoStrongBdd). The functional is carried on all of B(H); only its values on M are constrained (DIFFERENCES.md D1).

• toLinearMap : (H →L[ℂ] H) →ₗ[ℂ] ℂ

  The underlying linear functional.

• map_one' : self.toLinearMap 1 = 1
• nonneg' (x : H →L[ℂ] H) : x ∈ M → 0 ≤ self.toLinearMap (star x * x)
• normal' {κ : Type u} (l : Filter κ) (T : κ → H →L[ℂ] H) (L : H →L[ℂ] H) : (∀ (k : κ), T k ∈ M) → L ∈ M → CommutingRepetition.VN.TendstoStrongBdd l T L → Filter.Tendsto (fun (k : κ) => self.toLinearMap (T k)) l (nhds (self.toLinearMap L))

@[instance_reducible]

instance Orthogonalization.NormalState.instCoeFun {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} : CoeFun (NormalState M) fun (x : NormalState M) => (H →L[ℂ] H) → ℂ

Equations

• Orthogonalization.NormalState.instCoeFun = { coe := fun (φ : Orthogonalization.NormalState M) => ⇑φ.toLinearMap }

noncomputable def Orthogonalization.NormalState.normSq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} (φ : NormalState M) (x : H →L[ℂ] H) : ℝ

The square of the seminorm ‖a‖_φ = √φ(a*a) of Section 1 (defined there for elements of the algebra and a normal state; a real number, .re is lossless by positivity, DIFFERENCES.md D2).

Equations

• φ.normSq x = (φ.toLinearMap (star x * x)).re

theorem Orthogonalization.povm_orthogonalization {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (φ : NormalState M) {ι : Type u_1} [Fintype ι] (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 (thm:orthonormalization), the main result: a POVM (a_i) in a von Neumann algebra M with a normal state φ such that φ(∑ a_i²) > 1 − ε is 9ε-close to a PVM (p_i) ⊂ M: φ(∑ |a_i − p_i|²) < 9ε, where |a_i − p_i|² = (a_i − p_i)*(a_i − p_i).

theorem Orthogonalization.povm_orthogonalization_hilbert {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_1} [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), the Hilbert-space form: for a POVM (a_i) on H, a unit vector ξ and ε ∈ [0,1] with ∑ ‖a_i ξ‖² > 1 − ε, there is an orthogonal decomposition H = ⊕ H_i (given by its projections p_i, H_i = range p_i) such that (1) with ξ_i the orthogonal projection of ξ on H_i, ∑ ‖a_i ξ − ξ_i‖² < 9ε, and (2) every b ∈ B(H) commuting with each a_i preserves each H_i.

Proof-side helpers for Remark 1.3

The converse bound of Remark 1.3 is the triangle inequality for the seminorm ‖(b_i)‖_φ = √(∑ φ(b_i* b_i)) of tuples, for a functional positive on M only: p_i = a_i + (p_i − a_i) gives 1 = ∑ φ(p_i* p_i) ≤ (√φ(∑ a_i²) + √φ(∑ |a_i − p_i|²))². The helpers below (Cauchy–Schwarz in discriminant form and the squared triangle inequality) are proof-side only; they encode no statement of the paper.

theorem Orthogonalization.Converse.smul_mem_vn {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (c : ℂ) {z : H →L[ℂ] H} (hz : z ∈ M) : c • z ∈ M

Scalar multiples of elements of M lie in M.

theorem Orthogonalization.Converse.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.Converse.re_add_re_le_of_mem {H : Type u} [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.Converse.re_map_star_add_mul_add {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (x y : H →L[ℂ] H) : (φ (star (x + y) * (x + y))).re = (φ (star x * x)).re + (φ (star x * y)).re + (φ (star y * x)).re + (φ (star y * y)).re

Expansion of Re φ((x + y)* (x + y)).

theorem Orthogonalization.Converse.sum_re_add_le {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {ι : Type u_1} [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 functional positive on M only: if all b_i, c_i ∈ M, then ∑ ‖b_i + c_i‖_φ² ≤ (√(∑ ‖b_i‖_φ²) + √(∑ ‖c_i‖_φ²))².

theorem Orthogonalization.Converse.one_sub_two_sqrt_le {A D δ : ℝ} (hA : 0 ≤ A) (hD : 0 ≤ D) (hDδ : D ≤ δ) (h : 1 ≤ (√A + √D) ^ 2) : 1 - 2 * √δ ≤ A

Real arithmetic of Remark 1.3: from 1 ≤ (√A + √D)² with 0 ≤ A, 0 ≤ D ≤ δ, conclude 1 − 2 √δ ≤ A (via √A ≥ 1 − √δ, then squaring when 1 − √δ ≥ 0).

theorem Orthogonalization.povm_sq_ge_of_close_pvm {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (φ : NormalState M) {ι : Type u_1} [Fintype ι] (a p : ι → H →L[ℂ] H) (ha : IsPOVM M a) (hp : IsPVM M p) (δ : ℝ) (hδ : (φ.toLinearMap (∑ i : ι, star (a i - p i) * (a i - p i))).re ≤ δ) : 1 - 2 * √δ ≤ (φ.toLinearMap (∑ i : ι, a i * a i)).re

Remark 1.3, first display, second inequality (rem:9epsilon_optimal): conversely, if a PVM (p_i) satisfies ∑ φ(|a_i − p_i|²) ≤ δ then φ(∑ a_i²) ≥ 1 − 2√δ (the display's sharper intermediate bound (1 − √φ(∑|a_i − p_i|²))² is not stated; the ℓ∞² example of the remark is not formalized).

theorem Orthogonalization.pvm_almost_commute {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (φ : NormalState M) {ι : Type u_1} {κ : Type u_2} [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): almost commuting PVMs are close to commuting PVMs. If (p_i), (q_j) are PVMs in M with ∑_{i,j} ‖p_i q_j − q_j p_i‖_φ² < ε, there is a PVM (p'_i) in M with [p'_i, q_j] = 0 for all i, j and ∑_i ‖p_i − p'_i‖_φ² < 10ε.

theorem Orthogonalization.almost_commuting_unitaries {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (φ : NormalState M) (u v : H →L[ℂ] H) (hu : u ∈ M) (hv : v ∈ M) (hu' : u ∈ unitary (H →L[ℂ] H)) (hv' : v ∈ unitary (H →L[ℂ] H)) (n m : ℕ) (hn : 0 < n) (hm : 0 < m) (hun : u ^ n = 1) (hvm : v ^ m = 1) (ε : ℝ) (h : (↑n * ↑m)⁻¹ * ∑ i ∈ Finset.range n, ∑ j ∈ Finset.range m, φ.normSq (u ^ (i + 1) * v ^ (j + 1) - v ^ (j + 1) * u ^ (i + 1)) < ε) : ∃ v' ∈ M, v' ∈ unitary (H →L[ℂ] H) ∧ Commute u v' ∧ (↑m)⁻¹ * ∑ j ∈ Finset.range m, φ.normSq (v ^ (j + 1) - v' ^ (j + 1)) < 10 * ε

Corollary 1.5 (cor:almost_commuting): for unitaries u, v ∈ M of finite orders n, m with (nm)⁻¹ ∑_{i=1}^{n} ∑_{j=1}^{m} ‖u^i v^j − v^j u^i‖_φ² < ε, there is a unitary v' ∈ M commuting with u such that m⁻¹ ∑_{j=1}^{m} ‖v^j − v'^j‖_φ² < 10ε. (The paper's display normalizes the conclusion by n while summing powers of v; the average over the m powers of the approximated unitary v is what Theorem 1.4 and the Fourier dictionary of the paper yield — DIFFERENCES.md D5.)