theorem
CompleteGraphSpectrum.lapMatrix_completeGraph_mulVec
(n : ℕ)
(v : Fin n → ℝ)
:
(SimpleGraph.lapMatrix ℝ (SimpleGraph.completeGraph (Fin n))).mulVec v = fun (i : Fin n) => ↑n * v i - ∑ j : Fin n, v j
Instances For
theorem
CompleteGraphSpectrum.lemma15_complete_graph_spectrum
(n : ℕ)
(hn : 1 ≤ n)
:
Module.finrank ℝ ↥((completeGraphLapEnd n).eigenspace 0) = 1 ∧ ((completeGraphLapEnd n).eigenspace 0 = ℝ ∙ fun (x : Fin n) => 1) ∧ Module.finrank ℝ ↥((completeGraphLapEnd n).eigenspace ↑n) = n - 1 ∧ (completeGraphLapEnd n).eigenspace ↑n = (sumFunctional n).ker