@[implicit_reducible]

instance PathSpectrum.pathGraph_decRel (n : ℕ) : DecidableRel (SimpleGraph.pathGraph n).Adj

noncomputable def PathSpectrum.pathGraphEigenvalue (n : ℕ) (k : Fin n) : ℝ

noncomputable def PathSpectrum.pathGraphEigenvector (n : ℕ) (k u : Fin n) : ℝ

theorem PathSpectrum.eigenvector_interior (n : ℕ) (k u : Fin n) (h0 : 0 < ↑u) (hLast : ↑u + 1 < n) : (SimpleGraph.lapMatrix ℝ (SimpleGraph.pathGraph n)).mulVec (pathGraphEigenvector n k) u = pathGraphEigenvalue n k * pathGraphEigenvector n k u

theorem PathSpectrum.eigenvector_zero (n : ℕ) (hn : 2 ≤ n) (k : Fin n) : (SimpleGraph.lapMatrix ℝ (SimpleGraph.pathGraph n)).mulVec (pathGraphEigenvector n k) ⟨0, ⋯⟩ = pathGraphEigenvalue n k * pathGraphEigenvector n k ⟨0, ⋯⟩

theorem PathSpectrum.eigenvector_last (n : ℕ) (hn : 2 ≤ n) (k : Fin n) : (SimpleGraph.lapMatrix ℝ (SimpleGraph.pathGraph n)).mulVec (pathGraphEigenvector n k) ⟨n - 1, ⋯⟩ = pathGraphEigenvalue n k * pathGraphEigenvector n k ⟨n - 1, ⋯⟩

theorem PathSpectrum.pathGraph_lapMatrix_eigenvector (n : ℕ) (hn : 1 ≤ n) (k : Fin n) : (SimpleGraph.lapMatrix ℝ (SimpleGraph.pathGraph n)).mulVec (pathGraphEigenvector n k) = pathGraphEigenvalue n k • pathGraphEigenvector n k