Circulant matrices

DefinitionStandard primitive n-th root of unity \(e^{2\pi i/n}\)#✓fully proved

The exponential exp (2 * π * I / n), a primitive n-th root for nonzero n. This definition is total: at n = 0, it is exp 0 = 1.

noncomputable def zeta (n : ℕ) : ℂ := Complex.exp (2 * Real.pi * Complex.I / n)

Used by 6

Used byExponential-sum formula for circulant eigenvalues · Entrywise exponential formula for the Fourier matrix · Entrywise exponential formula for the inverse Fourier matrix · Exponential formula for Fourier vectors · Standard root of unity as the standard additive character · \(e^{2\pi i/n}\) is a primitive n-th root of unity

TheoremStandard root of unity as the standard additive character#✓fully proved

For nonzero n, zeta n is the canonical standard character at 1.

public theorem zeta_eq_stdAddChar : zeta n = ZMod.stdAddChar (1 : ZMod n)

Uses 1 · Used by 2

Statement usesStandard primitive n-th root of unity \(e^{2\pi i/n}\)

Used byExponential formula for Fourier vectors · \(e^{2\pi i/n}\) is a primitive n-th root of unity

Theorem\(e^{2\pi i/n}\) is a primitive n-th root of unity#✓fully proved

For nonzero n, the exponential is a primitive n-th root of unity.

public theorem zeta_isPrimitiveRoot : IsPrimitiveRoot (zeta n) n

Uses 2

Statement usesStandard primitive n-th root of unity \(e^{2\pi i/n}\)

Proof usesStandard root of unity as the standard additive character

DefinitionFourier vector on the integers modulo n#✓fully proved

The j-th Fourier vector on ZMod n, using the canonical positive character.

noncomputable def fourierVec (n : ℕ) [NeZero n] (j : ZMod n) : ZMod n → ℂ :=
  fun i => ZMod.stdAddChar (i * j)

Used by 4

Used byCirculant matrices are diagonalized by the Fourier matrix · Fourier vectors are eigenvectors of circulant matrices · Fourier matrix · Exponential formula for Fourier vectors

TheoremExponential formula for Fourier vectors#✓fully proved

The character definition of a Fourier vector agrees with its exponential formula.

public theorem fourierVec_apply (j i : ZMod n) :
    fourierVec n j i = zeta n ^ (i.val * j.val)

Uses 3 · Used by 3

Statement usesFourier vector on the integers modulo n · Standard primitive n-th root of unity \(e^{2\pi i/n}\)

Proof usesStandard root of unity as the standard additive character

Used byExponential-sum formula for circulant eigenvalues · Entrywise exponential formula for the Fourier matrix · Entrywise exponential formula for the inverse Fourier matrix

DefinitionFourier eigenvalue of a circulant matrix#✓fully proved

The j-th Fourier eigenvalue of a circulant matrix is its canonical DFT.

noncomputable def circulantEigenvalue (n : ℕ) [NeZero n] (v : ZMod n → ℂ) (j : ZMod n) : ℂ :=
  ZMod.dft v j

Used by 6

Used byExponential-sum formula for circulant eigenvalues · Zeroth circulant eigenvalue is the sum of entries · Circulant matrices are diagonalized by the Fourier matrix · Fourier vectors are eigenvectors of circulant matrices · Determinant of a circulant matrix · Sum of the eigenvalues of a circulant matrix

TheoremExponential-sum formula for circulant eigenvalues#✓fully proved

The canonical DFT definition agrees with the original negative-exponent eigenvalue sum.

public theorem circulantEigenvalue_apply (v : ZMod n → ℂ) (j : ZMod n) :
    circulantEigenvalue n v j = ∑ k, v k * zeta n ^ (-(k.val * j.val : ℤ))

Uses 3

Statement usesFourier eigenvalue of a circulant matrix · Standard primitive n-th root of unity \(e^{2\pi i/n}\)

Proof usesExponential formula for Fourier vectors

TheoremFourier vectors are eigenvectors of circulant matrices#✓fully proved

Every Fourier vector is an eigenvector of every circulant matrix.

public theorem circulant_mulVec_fourierVec (v : ZMod n → ℂ) (j : ZMod n) :
    Matrix.mulVec (Matrix.circulant v) (fourierVec n j) =
      circulantEigenvalue n v j • fourierVec n j

Uses 2 · Used by 1

Statement usesFourier eigenvalue of a circulant matrix · Fourier vector on the integers modulo n

Used byCirculant matrices are diagonalized by the Fourier matrix

DefinitionFourier matrix#✓fully proved

The Fourier matrix, whose j-th column is the standard character fourierVec n j.

noncomputable def fourierMatrix (n : ℕ) [NeZero n] : Matrix (ZMod n) (ZMod n) ℂ :=
  fun i j => fourierVec n j i

Uses 1 · Used by 5

Statement usesFourier vector on the integers modulo n

Used byCirculant matrices are diagonalized by the Fourier matrix · Determinant of a circulant matrix · Entrywise exponential formula for the Fourier matrix · Fourier matrix times its inverse is the identity · Fourier matrix acts as n times the inverse DFT

TheoremEntrywise exponential formula for the Fourier matrix#✓fully proved

The Fourier matrix agrees entrywise with its original exponential formula.

public theorem fourierMatrix_apply (i j : ZMod n) :
    fourierMatrix n i j = zeta n ^ (i.val * j.val)

Uses 3

Statement usesFourier matrix · Standard primitive n-th root of unity \(e^{2\pi i/n}\)

Proof usesExponential formula for Fourier vectors

DefinitionInverse Fourier matrix#✓fully proved

The inverse Fourier matrix, (1 / n) times the negative standard character.

noncomputable def fourierMatrixInv (n : ℕ) [NeZero n] : Matrix (ZMod n) (ZMod n) ℂ :=
  fun i j => (n : ℂ)⁻¹ * ZMod.stdAddChar (-(i * j))

Used by 4

Used byDeterminant of a circulant matrix · Entrywise exponential formula for the inverse Fourier matrix · Inverse Fourier matrix acts as the DFT divided by n · Fourier matrix times its inverse is the identity

TheoremEntrywise exponential formula for the inverse Fourier matrix#✓fully proved

The inverse Fourier matrix agrees entrywise with its original exponential formula.

public theorem fourierMatrixInv_apply (i j : ZMod n) :
    fourierMatrixInv n i j = (1 / (n : ℂ)) * zeta n ^ (-(i.val * j.val : ℤ))

Uses 3

Statement usesInverse Fourier matrix · Standard primitive n-th root of unity \(e^{2\pi i/n}\)

Proof usesExponential formula for Fourier vectors

TheoremFourier matrix acts as n times the inverse DFT#✓fully proved

Fourier matrix multiplication is the canonical inverse DFT multiplied by n.

public theorem fourierMatrix_mulVec_eq_invDFT (v : ZMod n → ℂ) :
    Matrix.mulVec (fourierMatrix n) v = (n : ℂ) • ZMod.dft.symm v

Uses 1 · Used by 1

Statement usesFourier matrix

Used byFourier matrix times its inverse is the identity

TheoremInverse Fourier matrix acts as the DFT divided by n#✓fully proved

Inverse Fourier matrix multiplication is the canonical DFT divided by n.

public theorem fourierMatrixInv_mulVec_eq_dft (v : ZMod n → ℂ) :
    Matrix.mulVec (fourierMatrixInv n) v = (n : ℂ)⁻¹ • ZMod.dft v

Uses 1 · Used by 1

Statement usesInverse Fourier matrix

Used byFourier matrix times its inverse is the identity

TheoremFourier matrix times its inverse is the identity#✓fully proved

The Fourier matrix is invertible, with inverse fourierMatrixInv.

public theorem fourierMatrix_mul_inv :
    fourierMatrix n * fourierMatrixInv n = (1 : Matrix (ZMod n) (ZMod n) ℂ)

Uses 4 · Used by 1

Statement usesFourier matrix · Inverse Fourier matrix

Proof usesInverse Fourier matrix acts as the DFT divided by n · Fourier matrix acts as n times the inverse DFT

Used byDeterminant of a circulant matrix

TheoremCirculant matrices are diagonalized by the Fourier matrix#✓fully proved

Circulant matrices are diagonalized by the Fourier matrix.

public theorem circulant_mul_fourierMatrix (v : ZMod n → ℂ) :
    Matrix.circulant v * fourierMatrix n =
      fourierMatrix n * Matrix.diagonal (circulantEigenvalue n v)

Uses 4 · Used by 1

Statement usesFourier eigenvalue of a circulant matrix · Fourier matrix

Proof usesFourier vectors are eigenvectors of circulant matrices · Fourier vector on the integers modulo n

Used byDeterminant of a circulant matrix

TheoremDeterminant of a circulant matrix#✓fully proved

The determinant of a circulant matrix is the product of its Fourier eigenvalues.

public theorem det_circulant (v : ZMod n → ℂ) :
    (Matrix.circulant v).det = ∏ j, circulantEigenvalue n v j

Uses 5

Statement usesFourier eigenvalue of a circulant matrix

Proof usesCirculant matrices are diagonalized by the Fourier matrix · Fourier matrix · Inverse Fourier matrix · Fourier matrix times its inverse is the identity

TheoremZeroth circulant eigenvalue is the sum of entries#✓fully proved

The Fourier eigenvalue at j = 0 is the sum of the entries of v.

public theorem circulantEigenvalue_zero (v : ZMod n → ℂ) :
    circulantEigenvalue n v 0 = ∑ k, v k

Uses 1

Statement usesFourier eigenvalue of a circulant matrix

TheoremSum of the eigenvalues of a circulant matrix#✓fully proved

The Fourier eigenvalues sum to n * v 0.

public theorem sum_circulantEigenvalue (v : ZMod n → ℂ) :
    ∑ j, circulantEigenvalue n v j = (n : ℂ) * v 0

Uses 1

Statement usesFourier eigenvalue of a circulant matrix

DefinitionBlock-circulant matrix over ℤ_n#✓fully proved

The block-circulant matrix on ℤ_n × Fin d with block v (p - q) in position (p, q).

def ons_blockCirculant (n d : ℕ) (v : ZMod n → Matrix (Fin d) (Fin d) ℂ) :
    Matrix ((ZMod n) × Fin d) ((ZMod n) × Fin d) ℂ :=
  fun p q => v (p.1 - q.1) p.2 q.2

DefinitionFourier symbol of a block-circulant matrix#✓fully proved

The Fourier symbol ∑_k ω ^ (k j) • v k of a block-circulant matrix at frequency j.

noncomputable def ons_blockSymbol (n d : ℕ) [NeZero n] (ω : ℂ)
    (v : ZMod n → Matrix (Fin d) (Fin d) ℂ)
    (j : ZMod n) : Matrix (Fin d) (Fin d) ℂ :=
  ∑ k : ZMod n, ω ^ ((k.val) * (j.val)) • v k

DefinitionTwo-dimensional block-circulant matrix on the torus#✓fully proved

The block-circulant matrix on (ℤ_L × ℤ_L) × Fin d with block v (p - q) in position (p, q).

def ons_blockCirculant2D (L d : ℕ) (v : (ZMod L × ZMod L) → Matrix (Fin d) (Fin d) ℂ) :
    Matrix ((ZMod L × ZMod L) × Fin d) ((ZMod L × ZMod L) × Fin d) ℂ :=
  fun p q => v (p.1.1 - q.1.1, p.1.2 - q.1.2) p.2 q.2

Used by 3

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Onsager's formula

DefinitionFourier symbol of a two-dimensional block-circulant matrix#✓fully proved

The Fourier symbol ∑_k ω ^ (k₁ j₁ + k₂ j₂) • v k at frequency j.

noncomputable def ons_blockSymbol2D (L d : ℕ) [NeZero L] (ω : ℂ)
    (v : (ZMod L × ZMod L) → Matrix (Fin d) (Fin d) ℂ) (j : ZMod L × ZMod L) :
    Matrix (Fin d) (Fin d) ℂ :=
  ∑ k : ZMod L × ZMod L, ω ^ (k.1.val * j.1.val + k.2.val * j.2.val) • v k

Used by 3

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Onsager's formula

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.