Documentation

Atlas.AnAlgorithmistsToolkit.code.SpectraCommonGraphs

@[reducible, inline]

abbrev SimpleGraph.cartesianProduct {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (H : SimpleGraph W) :

SimpleGraph (V × W)

Instances For

@[reducible, inline]

abbrev SpectraCommonGraphs.ringGraph (n : ℕ) :

SimpleGraph (Fin n)

Instances For

noncomputable def SpectraCommonGraphs.ringEigenvalue (n k : ℕ) :

Instances For

noncomputable def SpectraCommonGraphs.cosEigenvector (n k : ℕ) (u : Fin n) :

Instances For

noncomputable def SpectraCommonGraphs.sinEigenvector (n k : ℕ) (u : Fin n) :

Instances For

theorem SpectraCommonGraphs.cos_nat_mod_period (k n : ℕ) (hn : ↑n ≠ 0) (a : ℕ) :

Real.cos (2 * Real.pi * ↑k * ↑(a % n) / ↑n) = Real.cos (2 * Real.pi * ↑k * ↑a / ↑n)

theorem SpectraCommonGraphs.sin_nat_mod_period (k n : ℕ) (hn : ↑n ≠ 0) (a : ℕ) :

Real.sin (2 * Real.pi * ↑k * ↑(a % n) / ↑n) = Real.sin (2 * Real.pi * ↑k * ↑a / ↑n)

theorem SpectraCommonGraphs.cos_real_periodic_add (k m : ℕ) (hm : ↑m ≠ 0) (a : ℝ) :

Real.cos (2 * Real.pi * ↑k * (a + ↑m) / ↑m) = Real.cos (2 * Real.pi * ↑k * a / ↑m)

theorem SpectraCommonGraphs.sin_real_periodic_add (k m : ℕ) (hm : ↑m ≠ 0) (a : ℝ) :

Real.sin (2 * Real.pi * ↑k * (a + ↑m) / ↑m) = Real.sin (2 * Real.pi * ↑k * a / ↑m)

theorem SpectraCommonGraphs.fin_sub_one_ne_add_one {n : ℕ} (v : Fin (n + 3)) :

v - 1 ≠ v + 1

theorem SpectraCommonGraphs.lapMatrix_mulVec_cosEigenvector (n k : ℕ) :

(SimpleGraph.lapMatrix ℝ (ringGraph (n + 3))).mulVec (cosEigenvector (n + 3) k) = ringEigenvalue (n + 3) k • cosEigenvector (n + 3) k

theorem SpectraCommonGraphs.lapMatrix_mulVec_sinEigenvector (n k : ℕ) :

(SimpleGraph.lapMatrix ℝ (ringGraph (n + 3))).mulVec (sinEigenvector (n + 3) k) = ringEigenvalue (n + 3) k • sinEigenvector (n + 3) k

theorem SpectraCommonGraphs.ringGraph_lapMatrix_eigenvectors (n k : ℕ) :

(SimpleGraph.lapMatrix ℝ (ringGraph (n + 3))).mulVec (cosEigenvector (n + 3) k) = ringEigenvalue (n + 3) k • cosEigenvector (n + 3) k ∧ (SimpleGraph.lapMatrix ℝ (ringGraph (n + 3))).mulVec (sinEigenvector (n + 3) k) = ringEigenvalue (n + 3) k • sinEigenvector (n + 3) k

def GraphProductSpectrum.vecTensor {V : Type u_1} {W : Type u_2} (v : V → ℝ) (w : W → ℝ) :

V × W → ℝ

Instances For

theorem GraphProductSpectrum.kronecker_one_mulVec_tensor {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (A : Matrix V V ℝ) (v : V → ℝ) (w : W → ℝ) :

(Matrix.kroneckerMap (fun (x1 x2 : ℝ) => x1 * x2) A 1).mulVec (vecTensor v w) = vecTensor (A.mulVec v) w

theorem GraphProductSpectrum.one_kronecker_mulVec_tensor {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (B : Matrix W W ℝ) (v : V → ℝ) (w : W → ℝ) :

(Matrix.kroneckerMap (fun (x1 x2 : ℝ) => x1 * x2) 1 B).mulVec (vecTensor v w) = vecTensor v (B.mulVec w)

theorem GraphProductSpectrum.kronecker_sum_eigenvector {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (A : Matrix V V ℝ) (B : Matrix W W ℝ) (v : V → ℝ) (w : W → ℝ) (eigA eigB : ℝ) (hv : A.mulVec v = eigA • v) (hw : B.mulVec w = eigB • w) :

(Matrix.kroneckerMap (fun (x1 x2 : ℝ) => x1 * x2) A 1 + Matrix.kroneckerMap (fun (x1 x2 : ℝ) => x1 * x2) 1 B).mulVec (vecTensor v w) = (eigA + eigB) • vecTensor v w

@[implicit_reducible]

instance GraphProductSpectrum.boxProd_decidableAdj {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj] :

DecidableRel (G □ H).Adj

theorem GraphProductSpectrum.boxProd_degree_eq {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj] (v : V) (w : W) :

(G □ H).degree (v, w) = G.degree v + H.degree w

theorem GraphProductSpectrum.lapMatrix_boxProd_eq_kronecker_sum {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj] :

SimpleGraph.lapMatrix ℝ (G □ H) = Matrix.kroneckerMap (fun (x1 x2 : ℝ) => x1 * x2) (SimpleGraph.lapMatrix ℝ G) 1 + Matrix.kroneckerMap (fun (x1 x2 : ℝ) => x1 * x2) 1 (SimpleGraph.lapMatrix ℝ H)

theorem GraphProductSpectrum.lapMatrix_boxProd_eigenvector {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj] (v : V → ℝ) (w : W → ℝ) (eigG eigH : ℝ) (hv : (SimpleGraph.lapMatrix ℝ G).mulVec v = eigG • v) (hw : (SimpleGraph.lapMatrix ℝ H).mulVec w = eigH • w) :

(SimpleGraph.lapMatrix ℝ (G □ H)).mulVec (vecTensor v w) = (eigG + eigH) • vecTensor v w