def Matrix.IsEigenvectorOf {n : Type u_1} [Fintype n] (M : Matrix n n ℝ) (μ : ℝ) (x : n → ℝ) : Prop

noncomputable def Matrix.eigenspaceOf {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) (μ : ℝ) : Submodule ℝ (n → ℝ)

theorem EigenvalueBounds.trace_lapMatrix_eq_sum_degrees {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (SimpleGraph.lapMatrix ℝ G).trace = ∑ v : V, ↑(G.degree v)

theorem EigenvalueBounds.sum_eigenvalues₀_eq_sum_degrees {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : have hL := ⋯; ∑ i : Fin (Fintype.card V), hL.eigenvalues₀ i = ∑ v : V, ↑(G.degree v)

theorem EigenvalueBounds.sum_eigenvalues₀_eq_sum_degrees_le_maxDegree_mul_card {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : have hL := ⋯; ∑ i : Fin (Fintype.card V), hL.eigenvalues₀ i = ∑ v : V, ↑(G.degree v) ∧ ∑ v : V, ↑(G.degree v) ≤ ↑G.maxDegree * ↑(Fintype.card V)

theorem EigenvalueBounds.eigenvalues₀_min_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nonempty V] : have hL := ⋯; hL.eigenvalues₀ ⟨Fintype.card V - 1, ⋯⟩ = 0

theorem EigenvalueBounds.eigenvalue_second_smallest_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hn : Fintype.card V ≥ 2) : have hL := ⋯; let n := Fintype.card V; hL.eigenvalues₀ ⟨n - 2, ⋯⟩ ≤ (∑ v : V, ↑(G.degree v)) / (↑n - 1)

theorem EigenvalueBounds.eigenvalue_largest_ge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hn : Fintype.card V ≥ 2) : have hL := ⋯; have n := Fintype.card V; hL.eigenvalues₀ ⟨0, ⋯⟩ ≥ (∑ v : V, ↑(G.degree v)) / (↑n - 1)

theorem EigenvalueBounds.lemma22_eigenvalue_bounds {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hn : Fintype.card V ≥ 2) : have hL := ⋯; let n := Fintype.card V; hL.eigenvalues₀ ⟨n - 2, ⋯⟩ ≤ (∑ v : V, ↑(G.degree v)) / (↑n - 1) ∧ hL.eigenvalues₀ ⟨0, ⋯⟩ ≥ (∑ v : V, ↑(G.degree v)) / (↑n - 1)

theorem Matrix.eq_of_adj_of_lapMatrix_mulVec_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) (hx : (SimpleGraph.lapMatrix ℝ G).mulVec x = 0) (i j : V) (hadj : G.Adj i j) : x i = x j

theorem Matrix.eq_const_of_adj_eq_connected {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected) (x : V → ℝ) (hadj_eq : ∀ (i j : V), G.Adj i j → x i = x j) (v₀ w : V) : x w = x v₀

theorem Matrix.lapMatrix_eigenspace_zero_eq_span_ones {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected) : Module.End.eigenspace (SimpleGraph.lapMatrix ℝ G).mulVecLin 0 = ℝ ∙ fun (x : V) => 1

theorem EigenvalueBounds.eigenvalue_second_smallest_pos {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hn : Fintype.card V ≥ 2) (hconn : G.Connected) : have hL := ⋯; let n := Fintype.card V; 0 < hL.eigenvalues₀ ⟨n - 2, ⋯⟩