theorem Sparsification.loewner_order_iff_posSemidef {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] (M N : Matrix n n 𝕜) : N ≤ M ↔ (M - N).PosSemidef

def Sparsification.GraphLoewnerLE {V : Type u_3} [Fintype V] [DecidableEq V] (G H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] : Prop

def Sparsification.IsSpectralSparsifier {V : Type u_3} [Fintype V] [DecidableEq V] (G G' : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel G'.Adj] (ε : ℝ) : Prop

structure Sparsification.SymmWeights (V : Type u_4) : Type u_4

• w : V → V → ℝ
• symm (i j : V) : self.w i j = self.w j i
• diag_zero (i : V) : self.w i i = 0

noncomputable def Sparsification.weightedLapMatrix {V : Type u_3} [Fintype V] [DecidableEq V] (W : SymmWeights V) : Matrix V V ℝ

theorem Sparsification.weightedLap_inner_sum {V : Type u_3} [Fintype V] [DecidableEq V] (W : SymmWeights V) (x : V → ℝ) (i : V) : ∑ j : V, (if i = j then ∑ k : V, W.w i k else -W.w i j) * x j = (∑ k : V, W.w i k) * x i - ∑ j : V, W.w i j * x j

theorem Sparsification.weightedLap_quadform_eq {V : Type u_3} [Fintype V] [DecidableEq V] (W : SymmWeights V) (x : V → ℝ) : x ⬝ᵥ (weightedLapMatrix W).mulVec x = ∑ i : V, ∑ j : V, W.w i j * x i * (x i - x j)

theorem Sparsification.sum_swap_quadform {V : Type u_3} [Fintype V] (W : SymmWeights V) (x : V → ℝ) : ∑ i : V, ∑ j : V, W.w i j * x j * (x j - x i) = ∑ i : V, ∑ j : V, W.w i j * x i * (x i - x j)

theorem Sparsification.quadform_half_sum {V : Type u_3} [Fintype V] (W : SymmWeights V) (x : V → ℝ) : ∑ i : V, ∑ j : V, W.w i j * x i * (x i - x j) = 1 / 2 * ∑ i : V, ∑ j : V, W.w i j * (x i - x j) ^ 2

theorem Sparsification.weightedLapMatrix_posSemidef {V : Type u_3} [Fintype V] [DecidableEq V] (W : SymmWeights V) (hw : ∀ (i j : V), 0 ≤ W.w i j) : (weightedLapMatrix W).PosSemidef

theorem Sparsification.weightedLapMatrix_sub_eq {V : Type u_3} [Fintype V] [DecidableEq V] (W₁ W₂ : SymmWeights V) : weightedLapMatrix W₁ - weightedLapMatrix W₂ = weightedLapMatrix { w := fun (i j : V) => W₁.w i j - W₂.w i j, symm := ⋯, diag_zero := ⋯ }

theorem Sparsification.claim6_weight_monotone_loewner {V : Type u_3} [Fintype V] [DecidableEq V] (W_G W_H : SymmWeights V) (hw : ∀ (i j : V), W_H.w i j ≤ W_G.w i j) : weightedLapMatrix W_H ≤ weightedLapMatrix W_G

noncomputable def Sparsification.cutValue {V : Type u_3} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (S : Finset V) : ℕ

def Sparsification.IsNontrivialCut {V : Type u_3} [Fintype V] (S : Finset V) : Prop

noncomputable def Sparsification.minCutValue {V : Type u_3} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : ℕ

noncomputable def Sparsification.nontrivialCutsOfValueAtMost {V : Type u_3} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (k : ℕ) : Finset (Finset V)

theorem karger_cut_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (hc : 0 < Sparsification.minCutValue G) (α : ℝ) (hα : 1 ≤ α) : ↑(Sparsification.nontrivialCutsOfValueAtMost G ⌊α * ↑(Sparsification.minCutValue G)⌋₊).card ≤ ↑(Fintype.card V) ^ (2 * α)