Scalar facts: character orthogonality for a primitive root of unity

theorem Orthogonalization.sum_range_succ_shift {β : Type u_2} [AddCommGroup β] (f : ℕ → β) (N : ℕ) (h : f 0 = f N) : ∑ k ∈ Finset.range N, f (k + 1) = ∑ k ∈ Finset.range N, f k

Reindexing a sum over range N by k ↦ k + 1 for an N-periodic summand.

theorem Orthogonalization.star_zpow_of_isPrimitiveRoot {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) (z : ℤ) : star (ζ ^ z) = ζ ^ (-z)

The conjugate of an integer power of a root of unity is its inverse power.

theorem Orthogonalization.sum_zpow_mul_range {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (d : ℤ) : ∑ k ∈ Finset.range N, ζ ^ (d * ↑k) = if ↑N ∣ d then ↑N else 0

Character orthogonality: ∑_{k<N} ζ^{dk} = N if N ∣ d and 0 otherwise.

theorem Orthogonalization.sum_zpow_mul_fin {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (d : ℤ) : ∑ j : Fin N, ζ ^ (d * ↑↑j) = if ↑N ∣ d then ↑N else 0

Character orthogonality, summed over Fin N.

theorem Orthogonalization.natCast_dvd_sub_iff_fin {N : ℕ} (i i' : Fin N) : ↑N ∣ ↑↑i - ↑↑i' ↔ i = i'

Two elements of Fin N are congruent mod N only if they are equal.

theorem Orthogonalization.natCast_dvd_sub_iff_lt {N k k' : ℕ} (hk : k < N) (hk' : k' < N) : ↑N ∣ ↑k - ↑k' ↔ k = k'

Two elements of range N are congruent mod N only if they are equal.

Discrete Fourier coefficients in a star-algebra over ℂ

noncomputable def Orthogonalization.fourierCoeff {A : Type u_2} [Ring A] [Algebra ℂ A] (ζ : ℂ) (N : ℕ) (d : ℕ → A) (j : ℤ) : A

The j-th discrete Fourier coefficient N⁻¹ ∑_{l<N} ζ^{-jl} d l of a family d : ℕ → A (only the values d 0, …, d (N-1) matter).

Equations

• Orthogonalization.fourierCoeff ζ N d j = (↑N)⁻¹ • ∑ l ∈ Finset.range N, ζ ^ (-(j * ↑l)) • d l

theorem Orthogonalization.fourierCoeff_mul_right {A : Type u_2} [Ring A] [Algebra ℂ A] (ζ : ℂ) (N : ℕ) (d : ℕ → A) (j : ℤ) (y : A) : fourierCoeff ζ N d j * y = fourierCoeff ζ N (fun (l : ℕ) => d l * y) j

theorem Orthogonalization.fourierCoeff_mul_left {A : Type u_2} [Ring A] [Algebra ℂ A] (ζ : ℂ) (N : ℕ) (d : ℕ → A) (j : ℤ) (y : A) : y * fourierCoeff ζ N d j = fourierCoeff ζ N (fun (l : ℕ) => y * d l) j

theorem Orthogonalization.fourierCoeff_sub {A : Type u_2} [Ring A] [Algebra ℂ A] (ζ : ℂ) (N : ℕ) (d d' : ℕ → A) (j : ℤ) : fourierCoeff ζ N d j - fourierCoeff ζ N d' j = fourierCoeff ζ N (fun (l : ℕ) => d l - d' l) j

theorem Orthogonalization.fourierCoeff_swap {A : Type u_2} [Ring A] [Algebra ℂ A] (ζ : ℂ) (N : ℕ) (ω : ℂ) (N' : ℕ) (c : ℕ → ℕ → A) (i j : ℤ) : fourierCoeff ζ N (fun (l : ℕ) => fourierCoeff ω N' (fun (k : ℕ) => c k l) i) j = fourierCoeff ω N' (fun (k : ℕ) => fourierCoeff ζ N (fun (l : ℕ) => c k l) j) i

Two Fourier transforms in independent variables commute.

theorem Orthogonalization.sum_fourierCoeff_fourierCoeff_neg {A : Type u_2} [Ring A] [Algebra ℂ A] {ζ : ℂ} {N : ℕ} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) (F : ℕ → ℕ → A) : ∑ j : Fin N, fourierCoeff ζ N (fun (l' : ℕ) => fourierCoeff ζ N (fun (l : ℕ) => F l l') (-↑↑j)) ↑↑j = (↑N)⁻¹ • ∑ l ∈ Finset.range N, F l l

The orthogonality kernel of the Fourier transform: transforming twice, in the variables l and l', with opposite frequencies and summing over the frequency recovers the diagonal.

theorem Orthogonalization.star_fourierCoeff {A : Type u_2} [Ring A] [Algebra ℂ A] {ζ : ℂ} {N : ℕ} [StarRing A] [StarModule ℂ A] (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) (d : ℕ → A) (j : ℤ) : star (fourierCoeff ζ N d j) = fourierCoeff ζ N (fun (l : ℕ) => star (d l)) (-j)

The adjoint of a Fourier coefficient is the (-j)-th coefficient of the adjoints.

theorem Orthogonalization.sum_star_mul_fourierCoeff {A : Type u_2} [Ring A] [Algebra ℂ A] {ζ : ℂ} {N : ℕ} [StarRing A] [StarModule ℂ A] (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) (d : ℕ → A) : ∑ j : Fin N, star (fourierCoeff ζ N d ↑↑j) * fourierCoeff ζ N d ↑↑j = (↑N)⁻¹ • ∑ l ∈ Finset.range N, star (d l) * d l

Parseval's identity in the algebra: for the Fourier coefficients Y j = N⁻¹ ∑_{l<N} ζ^{-jl} d l, ∑_j (Y j)* (Y j) = N⁻¹ ∑_{l<N} (d l)* (d l).

The dictionary: spectral projections of a unitary of finite order

theorem Orthogonalization.pow_mul_eq_zpow_smul_of_mul_eq {A : Type u_2} [Ring A] [Algebra ℂ A] {ζ : ℂ} (hζ0 : ζ ≠ 0) {x p : A} {e : ℤ} (h : x * p = ζ ^ e • p) (l : ℕ) : x ^ l * p = ζ ^ (e * ↑l) • p

If x acts on p by the scalar ζ ^ e, then x ^ l acts by ζ ^ (e l).

theorem Orthogonalization.fourierCoeff_mul_of_eigen {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) {x : ℕ → A} {p : A} {e : ℤ} (h : ∀ (l : ℕ), x l * p = ζ ^ (e * ↑l) • p) (j : ℤ) : fourierCoeff ζ N x j * p = if ↑N ∣ e - j then p else 0

The Fourier coefficient of an eigenfamily: if x l * p = ζ ^ (e l) • p for every l, then (N⁻¹ ∑_{l<N} ζ^{-jl} x l) * p is p when j ≡ e (mod N) and 0 otherwise.

theorem Orthogonalization.smul_fourierCoeff {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} (c : ℂ) (d : ℕ → A) (j : ℤ) : c • fourierCoeff ζ N d j = fourierCoeff ζ N (fun (l : ℕ) => c • d l) j

Scalars pass through the Fourier transform.

noncomputable def Orthogonalization.spectralProj {A : Type u_2} [Ring A] [Algebra ℂ A] (ζ : ℂ) (N : ℕ) (w : A) (i : Fin N) : A

The spectral projections of a unitary w of order N (the paper's p_j = n⁻¹ ∑_k e^{-2ijkπ/n} u^k, line 149): P i = N⁻¹ ∑_{k<N} ζ^{-ik} w^k.

Equations

• Orthogonalization.spectralProj ζ N w i = Orthogonalization.fourierCoeff ζ N (fun (k : ℕ) => w ^ k) ↑↑i

theorem Orthogonalization.mul_spectralProj {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) {w : A} (hwN : w ^ N = 1) (i : Fin N) : w * spectralProj ζ N w i = ζ ^ ↑↑i • spectralProj ζ N w i

The eigen-relation w * P i = ζ ^ i • P i.

theorem Orthogonalization.pow_mul_spectralProj {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) {w : A} (hwN : w ^ N = 1) (i : Fin N) (l : ℕ) : w ^ l * spectralProj ζ N w i = ζ ^ (↑↑i * ↑l) • spectralProj ζ N w i

The powers of w act on P i by ζ ^ (i l).

theorem Orthogonalization.spectralProj_mul_spectralProj {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) {w : A} (hwN : w ^ N = 1) (i' i : Fin N) : spectralProj ζ N w i' * spectralProj ζ N w i = if i' = i then spectralProj ζ N w i else 0

The spectral projections are pairwise orthogonal idempotents: P i' * P i = δ_{i' i} P i.

theorem Orthogonalization.sum_spectralProj {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) {w : A} : ∑ i : Fin N, spectralProj ζ N w i = 1

The spectral projections sum to 1.

theorem Orthogonalization.eq_sum_zpow_smul_spectralProj {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) {w : A} (hwN : w ^ N = 1) : w = ∑ i : Fin N, ζ ^ ↑↑i • spectralProj ζ N w i

The inverse Fourier transform: w = ∑_i ζ^i P i (the paper's u = ∑_k e^{2ikπ/n} p_k).

theorem Orthogonalization.star_spectralProj_mul_spectralProj {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) {w : A} (hwN : w ^ N = 1) [StarRing A] [StarModule ℂ A] (hw : star w * w = 1) (i i' : Fin N) : star (spectralProj ζ N w i) * spectralProj ζ N w i' = if i = i' then spectralProj ζ N w i' else 0

P i* P i' = δ_{i i'} P i' (using w* = w⁻¹).

theorem Orthogonalization.star_spectralProj {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) {w : A} (hwN : w ^ N = 1) [StarRing A] [StarModule ℂ A] (hw : star w * w = 1) (i : Fin N) : star (spectralProj ζ N w i) = spectralProj ζ N w i

The spectral projections are self-adjoint.

theorem Orthogonalization.isStarProjection_spectralProj {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) {w : A} (hwN : w ^ N = 1) [StarRing A] [StarModule ℂ A] (hw : star w * w = 1) (i : Fin N) : IsStarProjection (spectralProj ζ N w i)

The spectral projections are (star) projections.

The inverse dictionary: the unitary of an orthogonal family of projections

noncomputable def Orthogonalization.fourierUnitary {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} (ζ : ℂ) (r : Fin N → A) : A

The unitary ∑_j ζ^j r j of a family r of projections (the paper's u = ∑_k e^{2ikπ/n} p_k, line 149).

Equations

• Orthogonalization.fourierUnitary ζ r = ∑ j : Fin N, ζ ^ ↑↑j • r j

theorem Orthogonalization.fourierUnitary_mul {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} {r : Fin N → A} (horth : ∀ (j' j : Fin N), r j' * r j = if j' = j then r j else 0) (j : Fin N) : fourierUnitary ζ r * r j = ζ ^ ↑↑j • r j

theorem Orthogonalization.mul_fourierUnitary {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} {r : Fin N → A} (horth : ∀ (j' j : Fin N), r j' * r j = if j' = j then r j else 0) (j : Fin N) : r j * fourierUnitary ζ r = ζ ^ ↑↑j • r j

theorem Orthogonalization.pow_fourierUnitary_mul {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} {r : Fin N → A} (horth : ∀ (j' j : Fin N), r j' * r j = if j' = j then r j else 0) (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) (j : Fin N) (l : ℕ) : fourierUnitary ζ r ^ l * r j = ζ ^ (↑↑j * ↑l) • r j

theorem Orthogonalization.fourierUnitary_pow {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} {r : Fin N → A} (horth : ∀ (j' j : Fin N), r j' * r j = if j' = j then r j else 0) (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) (hsum : ∑ j : Fin N, r j = 1) (l : ℕ) : fourierUnitary ζ r ^ l = ∑ j : Fin N, ζ ^ (↑↑j * ↑l) • r j

The powers of the reconstructed unitary: (∑_j ζ^j r j)^l = ∑_j ζ^{jl} r j.

theorem Orthogonalization.fourierUnitary_pow_eq_one {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} {r : Fin N → A} (horth : ∀ (j' j : Fin N), r j' * r j = if j' = j then r j else 0) (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) (hsum : ∑ j : Fin N, r j = 1) : fourierUnitary ζ r ^ N = 1

The reconstructed unitary has order dividing N.

theorem Orthogonalization.spectralProj_fourierUnitary {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} {r : Fin N → A} (horth : ∀ (j' j : Fin N), r j' * r j = if j' = j then r j else 0) (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) (hsum : ∑ j : Fin N, r j = 1) (j : Fin N) : spectralProj ζ N (fourierUnitary ζ r) j = r j

The spectral projections of the reconstructed unitary are the original projections.

theorem Orthogonalization.star_fourierUnitary {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} {r : Fin N → A} (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) [StarRing A] [StarModule ℂ A] (hsa : ∀ (j : Fin N), star (r j) = r j) : star (fourierUnitary ζ r) = ∑ j : Fin N, ζ ^ (-↑↑j) • r j

theorem Orthogonalization.star_fourierUnitary_mul_self {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} {r : Fin N → A} (horth : ∀ (j' j : Fin N), r j' * r j = if j' = j then r j else 0) (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) (hsum : ∑ j : Fin N, r j = 1) [StarRing A] [StarModule ℂ A] (hsa : ∀ (j : Fin N), star (r j) = r j) : star (fourierUnitary ζ r) * fourierUnitary ζ r = 1

theorem Orthogonalization.fourierUnitary_mul_star_self {A : Type u_2} [Ring A] [Algebra ℂ A] {N : ℕ} {ζ : ℂ} {r : Fin N → A} (horth : ∀ (j' j : Fin N), r j' * r j = if j' = j then r j else 0) (hζ : IsPrimitiveRoot ζ N) (hN : 0 < N) (hsum : ∑ j : Fin N, r j = 1) [StarRing A] [StarModule ℂ A] (hsa : ∀ (j : Fin N), star (r j) = r j) : fourierUnitary ζ r * star (fourierUnitary ζ r) = 1

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

theorem Orthogonalization.IsPVM.mul_eq_ite {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ 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. (From q j = q j (∑ k, q k) q j = q j + ∑_{k ≠ j} (q k q j)* (q k q j) and positivity.)

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

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

theorem Orthogonalization.isPVM_spectralProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ 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] [FiniteDimensional ℂ 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] [FiniteDimensional ℂ 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] [FiniteDimensional ℂ 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}‖_φ².

Corollary 1.5 in finite dimension

theorem Orthogonalization.almost_commuting_unitaries_finDim {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ 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) in finite dimension.