noncomputable def Matrix.IsHermitian.spectralRadius {n : ℕ} {M : Matrix (Fin n) (Fin n) ℝ} (hM : M.IsHermitian) : ℝ

noncomputable def An_Algorithmists_Toolkit.energyNorm {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (e : Fin n → ℝ) : ℝ

theorem An_Algorithmists_Toolkit.fin_telescope_sum (k : ℕ) (f : Fin (k + 1) → ℝ) : ∑ i : Fin k, (f i.castSucc - f i.succ) = f 0 - f (Fin.last k)

theorem An_Algorithmists_Toolkit.edge_loewner_path {n : ℕ} (k : ℕ) (hk : 0 < k) (path : Fin (k + 1) → Fin n) (hinj : Function.Injective path) (u v : Fin n) (hu : path 0 = u) (hv : path ⟨k, ⋯⟩ = v) (L_e L_path : Matrix (Fin n) (Fin n) ℝ) (hLe : ∀ (x : Fin n → ℝ), x ⬝ᵥ L_e.mulVec x = (x u - x v) ^ 2) (hLp : ∀ (x : Fin n → ℝ), x ⬝ᵥ L_path.mulVec x = ∑ i : Fin k, (x (path i.castSucc) - x (path i.succ)) ^ 2) (x : Fin n → ℝ) : x ⬝ᵥ L_e.mulVec x ≤ ↑k * x ⬝ᵥ L_path.mulVec x

theorem An_Algorithmists_Toolkit.steepest_descent_error_reduction {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA_pd : A.PosDef) (eigenvalues : Fin n → ℝ) (eigenvectors : Fin n → Fin n → ℝ) (hev : ∀ (i : Fin n), A.mulVec (eigenvectors i) = eigenvalues i • eigenvectors i) (horth : ∀ (i j : Fin n), eigenvectors i ⬝ᵥ eigenvectors j = if i = j then 1 else 0) (e_i ξ : Fin n → ℝ) (hξ : e_i = ∑ j : Fin n, ξ j • eigenvectors j) (e_next : Fin n → ℝ) (he_next : e_next = e_i - (A.mulVec e_i ⬝ᵥ A.mulVec e_i / A.mulVec e_i ⬝ᵥ A.mulVec (A.mulVec e_i)) • A.mulVec e_i) : energyNorm A e_next = energyNorm A e_i * (1 - (∑ j : Fin n, ξ j ^ 2 * eigenvalues j ^ 2) ^ 2 / ((∑ j : Fin n, ξ j ^ 2 * eigenvalues j ^ 3) * ∑ j : Fin n, ξ j ^ 2 * eigenvalues j))

theorem An_Algorithmists_Toolkit.steepest_descent_eigenvector_convergence {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (e_i : Fin n → ℝ) (he_nz : e_i ≠ 0) (μ : ℝ) (hμ : μ ≠ 0) (heig : A.mulVec e_i = μ • e_i) (e_next : Fin n → ℝ) (he_next : e_next = e_i - (A.mulVec e_i ⬝ᵥ A.mulVec e_i / A.mulVec e_i ⬝ᵥ A.mulVec (A.mulVec e_i)) • A.mulVec e_i) : e_next = 0

theorem An_Algorithmists_Toolkit.iter_error_step {n : ℕ} (A L S : Matrix (Fin n) (Fin n) ℝ) (hA : A = L + S) [Invertible L] (b x_star : Fin n → ℝ) (hx : A.mulVec x_star = b) (xk : Fin n → ℝ) : (⅟L).mulVec (b - S.mulVec xk) - x_star = -(⅟L * S).mulVec (xk - x_star)

theorem An_Algorithmists_Toolkit.iterative_solver_convergence {n : ℕ} (A L S : Matrix (Fin n) (Fin n) ℝ) (hA : A = L + S) [Invertible L] (ρ : ℝ) (hρ : ρ < 1) (hρ_pos : 0 ≤ ρ) (hρ_spec : ∀ (v : Fin n → ℝ), ‖(⅟L * S).mulVec v‖ ≤ ρ * ‖v‖) (b x_star : Fin n → ℝ) (hx : A.mulVec x_star = b) (x : ℕ → Fin n → ℝ) (hiter : ∀ (k : ℕ), x (k + 1) = (⅟L).mulVec (b - S.mulVec (x k))) (k : ℕ) : ‖x k - x_star‖ ≤ ρ ^ k * ‖x 0 - x_star‖

noncomputable def LowStretchSpanningTree.total_stretch {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] (T : SimpleGraph V) : ℕ

noncomputable def LowStretchSpanningTree.low_stretch_exponent : ℝ

theorem LowStretchSpanningTree.low_stretch_spanning_tree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (hG : G.Connected) : ∃ (T : SimpleGraph V), T.IsTree ∧ T ≤ G ∧ ↑(total_stretch G T) ≤ ↑G.edgeFinset.card * Real.log ↑(Fintype.card V) ^ low_stretch_exponent

theorem spectral_sparsifier_near_linear {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (t : ℝ) (ht : 0 < t) : ∃ (H : SimpleGraph V) (x : DecidableRel H.Adj) (x_1 : Fintype ↑H.edgeSet), (∃ (C : ℕ), ↑H.edgeFinset.card ≤ ↑(Fintype.card V) + t * Real.log ↑(Fintype.card V) ^ C) ∧ SimpleGraph.lapMatrix ℝ H ≤ SimpleGraph.lapMatrix ℝ G ∧ SimpleGraph.lapMatrix ℝ G ≤ (↑(Fintype.card V) / t) • SimpleGraph.lapMatrix ℝ H