@[reducible, inline]

noncomputable abbrev GraphMatrices.adjMatrix {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] : Matrix V V ℝ

theorem GraphMatrices.laplacian_mulVec_ones_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ((SimpleGraph.lapMatrix ℝ G).mulVec fun (x : V) => 1) = 0

theorem GraphMatrices.laplacian_posSemidef {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (SimpleGraph.lapMatrix ℝ G).PosSemidef

theorem GraphMatrices.laplacian_proposition_6 {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ((SimpleGraph.lapMatrix ℝ G).mulVec fun (x : V) => 1) = 0 ∧ (SimpleGraph.lapMatrix ℝ G).PosSemidef

structure GraphMatrices.EdgeOrientation {V : Type u_1} (G : SimpleGraph V) : Type u_1

• orient : ↑G.edgeSet → V × V
• edge_eq (e : ↑G.edgeSet) : s((self.orient e).1, (self.orient e).2) = ↑e

theorem GraphMatrices.sum_incident_eq_degree {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (i : V) : (∑ e : ↑G.edgeSet, if i ∈ ↑e then 1 else 0) = ↑(G.degree i)

noncomputable def GraphMatrices.signedIncidenceMatrix {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (σ : EdgeOrientation G) : Matrix (↑G.edgeSet) V ℝ

theorem GraphMatrices.lapMatrix_eq_transpose_mul_signedIncMatrix {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (σ : EdgeOrientation G) : SimpleGraph.lapMatrix ℝ G = (signedIncidenceMatrix σ).transpose * signedIncidenceMatrix σ

theorem GraphMatrices.double_sum_adj_eq_dart_sum {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (f : V → V → ℝ) : (∑ i : V, ∑ j : V, if G.Adj i j then f i j else 0) = ∑ d : G.Dart, f d.toProd.1 d.toProd.2

theorem GraphMatrices.dart_sum_eq_twice_edge_sum {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (f : V → V → ℝ) (hf : ∀ (a b : V), f a b = f b a) : ∑ d : G.Dart, f d.toProd.1 d.toProd.2 = 2 * ∑ e ∈ G.edgeFinset, Sym2.lift ⟨f, ⋯⟩ e

theorem GraphMatrices.sum_adj_div_two_eq_sum_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (f : V → V → ℝ) (hf : ∀ (a b : V), f a b = f b a) : (∑ i : V, ∑ j : V, if G.Adj i j then f i j else 0) / 2 = ∑ e ∈ G.edgeFinset, Sym2.lift ⟨f, ⋯⟩ e

theorem GraphMatrices.lapMatrix_quadForm_eq_sum_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (x : V → ℝ) : x ⬝ᵥ (SimpleGraph.lapMatrix ℝ G).mulVec x = ∑ e ∈ G.edgeFinset, Sym2.lift ⟨fun (i j : V) => (x i - x j) ^ 2, ⋯⟩ e

theorem GraphMatrices.lapMatrix_quadForm_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (x : V → ℝ) : 0 ≤ x ⬝ᵥ (SimpleGraph.lapMatrix ℝ G).mulVec x