@[reducible, inline]

abbrev PSDMatrix.IsPSD {n : Type u_1} (M : Matrix n n ℝ) : Prop

@[reducible, inline]

abbrev PSDMatrix.IsPD {n : Type u_1} (M : Matrix n n ℝ) : Prop

theorem PSDMatrix.isPSD_iff_eigenvalues_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M.IsHermitian) : IsPSD M ↔ ∀ (i : n), 0 ≤ hM.eigenvalues i

theorem PSDMatrix.isPD_iff_eigenvalues_pos {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M.IsHermitian) : IsPD M ↔ ∀ (i : n), 0 < hM.eigenvalues i

theorem PSDMatrix.isPSD_and_isPD_iff_eigenvalues {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M.IsHermitian) : (IsPSD M ↔ ∀ (i : n), 0 ≤ hM.eigenvalues i) ∧ (IsPD M ↔ ∀ (i : n), 0 < hM.eigenvalues i)

theorem PSDMatrix.star_eq_transpose {n : Type u_1} [Fintype n] [DecidableEq n] (B : Matrix n n ℝ) : star B = B.transpose

theorem PSDMatrix.conjTranspose_eq_transpose_real {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] (B : Matrix m n ℝ) : B.conjTranspose = B.transpose

theorem PSDMatrix.isPSD_iff_exists_transpose_mul_self {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) : IsPSD M ↔ ∃ (B : Matrix n n ℝ), M = B.transpose * B

theorem PSDMatrix.isPSD_iff_exists_transpose_mul_self_rect {n : Type u_psd} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) : IsPSD M ↔ ∃ (k : Type u_psd) (x : Fintype k) (B : Matrix k n ℝ), M = B.transpose * B

theorem LaplacianProperties.eq_of_adj_of_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 LaplacianProperties.eq_const_of_adj_eq {V : Type u_1} (G : SimpleGraph V) (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 LaplacianProperties.ker_lapMatrix_eq_span_ones {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected) : (SimpleGraph.lapMatrix ℝ G).mulVecLin.ker = ℝ ∙ fun (x : V) => 1

theorem LaplacianProperties.adjMatrix_sup_of_disjoint {V : Type u_3} [Fintype V] [DecidableEq V] (G H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] (hd : Disjoint G H) : SimpleGraph.adjMatrix ℝ (G ⊔ H) = SimpleGraph.adjMatrix ℝ G + SimpleGraph.adjMatrix ℝ H

theorem LaplacianProperties.degree_sup_of_disjoint {V : Type u_3} [Fintype V] [DecidableEq V] (G H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] (hd : Disjoint G H) (v : V) : (G ⊔ H).degree v = G.degree v + H.degree v

theorem LaplacianProperties.degMatrix_sup_of_disjoint {V : Type u_3} [Fintype V] [DecidableEq V] (G H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] (hd : Disjoint G H) : SimpleGraph.degMatrix ℝ (G ⊔ H) = SimpleGraph.degMatrix ℝ G + SimpleGraph.degMatrix ℝ H

theorem LaplacianProperties.lapMatrix_sup_of_disjoint {V : Type u_3} [Fintype V] [DecidableEq V] (G H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] (hd : Disjoint G H) : SimpleGraph.lapMatrix ℝ (G ⊔ H) = SimpleGraph.lapMatrix ℝ G + SimpleGraph.lapMatrix ℝ H

theorem LaplacianProperties.not_adj_of_degree_zero {V : Type u_2} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {v : V} (hdeg : G.degree v = 0) (j : V) : ¬G.Adj v j

theorem LaplacianProperties.lapMatrix_row_eq_zero_of_degree_zero {V : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {v : V} (hdeg : G.degree v = 0) (j : V) : SimpleGraph.lapMatrix ℝ G v j = 0

theorem LaplacianProperties.lapMatrix_col_eq_zero_of_degree_zero {V : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {v : V} (hdeg : G.degree v = 0) (j : V) : SimpleGraph.lapMatrix ℝ G j v = 0

theorem LaplacianProperties.lapMatrix_eq_zero_of_degree_zero {V : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {v : V} (hdeg : G.degree v = 0) (j : V) : SimpleGraph.lapMatrix ℝ G v j = 0 ∧ SimpleGraph.lapMatrix ℝ G j v = 0

theorem LaplacianProperties.dim_ker_lapMatrix_eq_card_connectedComponent {V : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Module.finrank ℝ ↥(SimpleGraph.lapMatrix ℝ G).mulVecLin.ker = Fintype.card G.ConnectedComponent