Operators on any complete H: PVMs, membership in M, and Parseval for ‖·‖_φ

The [CompleteSpace H] versions of the Operators section of Blocks/Fourier.lean (there stated under [FiniteDimensional ℂ H]; the proofs are unchanged).

theorem Orthogonalization.IsPVM.mul_eq_ite' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {N : ℕ} {q : Fin N → H →L[ℂ] H} (hq : IsPVM M q) (j' j : Fin N) : q j' * q j = if j' = j then q j else 0

The projections of a PVM are pairwise orthogonal: q j' * q j = δ_{j' j} q j (IsPVM.mul_eq_ite of Blocks/Fourier.lean on any complete H).

theorem Orthogonalization.spectralProj_mem' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {N : ℕ} {ζ : ℂ} (M : VonNeumannAlgebra H) {w : H →L[ℂ] H} (hw : w ∈ M) (i : Fin N) : spectralProj ζ N w i ∈ M

The spectral projections of w ∈ M lie in M.

theorem Orthogonalization.fourierUnitary_mem' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {N : ℕ} {ζ : ℂ} (M : VonNeumannAlgebra H) {r : Fin N → H →L[ℂ] H} (hr : ∀ (j : Fin N), r j ∈ M) : fourierUnitary ζ r ∈ M

The reconstructed unitary of a family of elements of M lies in M.

theorem Orthogonalization.isPVM_spectralProj' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {N : ℕ} {ζ : ℂ} (M : VonNeumannAlgebra H) (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) {w : H →L[ℂ] H} (hw : w ∈ M) (hw1 : star w * w = 1) (hwN : w ^ N = 1) : IsPVM M (spectralProj ζ N w)

The spectral projections of a unitary w ∈ M of order N form a PVM in M.

theorem Orthogonalization.NormalState.normSq_neg' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} (φ : NormalState M) (x : H →L[ℂ] H) : φ.normSq (-x) = φ.normSq x

‖-x‖_φ² = ‖x‖_φ².

theorem Orthogonalization.sum_normSq_fourierCoeff' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {N : ℕ} {ζ : ℂ} {M : VonNeumannAlgebra H} (φ : NormalState M) (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) (d : ℕ → H →L[ℂ] H) : ∑ j : Fin N, φ.normSq (fourierCoeff ζ N d ↑↑j) = (↑N)⁻¹ * ∑ l ∈ Finset.range N, φ.normSq (d l)

Parseval for the seminorm ‖·‖_φ: ∑_j ‖Y j‖_φ² = N⁻¹ ∑_{l<N} ‖d l‖_φ² for the Fourier coefficients Y j = N⁻¹ ∑_{l<N} ζ^{-jl} d l (only linearity of φ is used).

theorem Orthogonalization.sum_normSq_spectralProj_comm' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} (φ : NormalState M) {n m : ℕ} {ω ζ : ℂ} (hω : IsPrimitiveRoot ω n) (hn : 0 < n) (hζ : IsPrimitiveRoot ζ m) (hm : 0 < m) {u v : H →L[ℂ] H} (hun : u ^ n = 1) (hvm : v ^ m = 1) : ∑ i : Fin n, ∑ j : Fin m, φ.normSq (spectralProj ω n u i * spectralProj ζ m v j - spectralProj ζ m v j * spectralProj ω n u i) = (↑n * ↑m)⁻¹ * ∑ k ∈ Finset.range n, ∑ l ∈ Finset.range m, φ.normSq (u ^ (k + 1) * v ^ (l + 1) - v ^ (l + 1) * u ^ (k + 1))

The hypothesis of Corollary 1.5 is the hypothesis of Theorem 1.4 for the spectral PVMs: ∑_{i,j} ‖p_i q_j − q_j p_i‖_φ² = (nm)⁻¹ ∑_{k<n} ∑_{l<m} ‖u^{k+1} v^{l+1} − v^{l+1} u^{k+1}‖_φ².

Theorem 1.1

theorem Orthogonalization.povm_orthogonalization_hilbert_of_structure (hS : MvNStructureTheory) {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, conditional form (thm:orthonormalization_Hilbert; tier T3): the statement of povm_orthogonalization_hilbert on every complex Hilbert space, with the commutant clause, under the structure-theory interface. Proof: Theorem 1.2 (povm_orthogonalization_of_structure) 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 1.4

theorem Orthogonalization.pvm_almost_commute_of_structure (hS : MvNStructureTheory) {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, conditional form (thm:pvm_almost_commute; tier T3): the statement of pvm_almost_commute for every von Neumann algebra, under the structure-theory interface. 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 (povm_orthogonalization_of_structure) 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.

Corollary 1.5

theorem Orthogonalization.almost_commuting_unitaries_of_structure (hS : MvNStructureTheory) {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, conditional form (cor:almost_commuting; tier T3): the statement of almost_commuting_unitaries for every von Neumann algebra, under the structure-theory interface (conclusion normalized as in DIFFERENCES.md D5). Proof: the paper's Fourier dictionary (Blocks/Fourier.lean) converts the hypothesis and the conclusion of Theorem 1.4 (pvm_almost_commute_of_structure, applied with the spectral PVM of v in the perturbed slot) into those of Corollary 1.5.