theorem CourantFischer.eucl_inner_eq_dotProduct {V : Type u_1} [Fintype V] (a b : EuclideanSpace ℝ V) : inner ℝ a b = a.ofLp ⬝ᵥ b.ofLp

theorem CourantFischer.rayleigh_spectral_expansion {m : ℕ} {A : Matrix (Fin m) (Fin m) ℝ} (hA : A.IsHermitian) (x : Fin m → ℝ) : x ⬝ᵥ A.mulVec x = ∑ i : Fin m, hA.eigenvalues i * ((hA.eigenvectorBasis i).ofLp ⬝ᵥ x) ^ 2

theorem CourantFischer.parseval_eigenvectors {m : ℕ} {A : Matrix (Fin m) (Fin m) ℝ} (hA : A.IsHermitian) (x : Fin m → ℝ) : ∑ i : Fin m, ((hA.eigenvectorBasis i).ofLp ⬝ᵥ x) ^ 2 = x ⬝ᵥ x

theorem CourantFischer.eigenvalues_antitone {m : ℕ} {A : Matrix (Fin m) (Fin m) ℝ} (hA : A.IsHermitian) (i j : Fin m) (hij : i ≤ j) : hA.eigenvalues j ≤ hA.eigenvalues i

theorem CourantFischer.rayleigh_le_eigenvalue_orthogonal {m : ℕ} {A : Matrix (Fin m) (Fin m) ℝ} (hA : A.IsHermitian) (k : Fin m) (x : Fin m → ℝ) (hx : x ⬝ᵥ x = 1) (horth : ∀ j < k, (hA.eigenvectorBasis j).ofLp ⬝ᵥ x = 0) : x ⬝ᵥ A.mulVec x ≤ hA.eigenvalues k

theorem CourantFischer.rayleigh_spectral_expansion_V {V : Type u_1} [Fintype V] [DecidableEq V] {L : Matrix V V ℝ} (hL : L.IsHermitian) (x : V → ℝ) : x ⬝ᵥ L.mulVec x = ∑ i : V, hL.eigenvalues i * ((hL.eigenvectorBasis i).ofLp ⬝ᵥ x) ^ 2

theorem CourantFischer.parseval_eigenvectors_V {V : Type u_1} [Fintype V] [DecidableEq V] {L : Matrix V V ℝ} (hL : L.IsHermitian) (x : V → ℝ) : ∑ i : V, ((hL.eigenvectorBasis i).ofLp ⬝ᵥ x) ^ 2 = x ⬝ᵥ x

theorem CourantFischer.eigenvalue_eq_rayleigh_eigenvector_V {V : Type u_1} [Fintype V] [DecidableEq V] {L : Matrix V V ℝ} (hL : L.IsHermitian) (k : V) : (hL.eigenvectorBasis k).ofLp ⬝ᵥ L.mulVec (hL.eigenvectorBasis k).ofLp = hL.eigenvalues k

theorem CourantFischer.eigenvector_dotProduct_one_V {V : Type u_1} [Fintype V] [DecidableEq V] {L : Matrix V V ℝ} (hL : L.IsHermitian) (k : V) : (hL.eigenvectorBasis k).ofLp ⬝ᵥ (hL.eigenvectorBasis k).ofLp = 1

theorem CourantFischer.rayleighQuotient_orthogonal_isLeast {V : Type u_1} [Fintype V] [DecidableEq V] {L : Matrix V V ℝ} (hL : L.IsHermitian) (k : V) : IsLeast {r : ℝ | ∃ (x : V → ℝ), x ≠ 0 ∧ (∀ (j : V), hL.eigenvalues j < hL.eigenvalues k → (hL.eigenvectorBasis j).ofLp ⬝ᵥ x = 0) ∧ x ⬝ᵥ L.mulVec x / x ⬝ᵥ x = r} (hL.eigenvalues k)

theorem CourantFischer.laplacian_quadratic_form_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) : x ⬝ᵥ (SimpleGraph.lapMatrix ℝ G).mulVec x = (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

theorem CourantFischer.laplacian_edge_sum_min_characterization {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hL : (SimpleGraph.lapMatrix ℝ G).IsHermitian) (k : V) : IsLeast {r : ℝ | ∃ (x : V → ℝ), x ≠ 0 ∧ (∀ (j : V), hL.eigenvalues j < hL.eigenvalues k → (hL.eigenvectorBasis j).ofLp ⬝ᵥ x = 0) ∧ (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2 / x ⬝ᵥ x = r} (hL.eigenvalues k)

theorem CourantFischer.laplacian_edge_sum_max_quotient_characterization {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hL : (SimpleGraph.lapMatrix ℝ G).IsHermitian) (i₀ : V) (hi₀ : ∀ (j : V), hL.eigenvalues j ≤ hL.eigenvalues i₀) : IsGreatest {r : ℝ | ∃ (x : V → ℝ), x ≠ 0 ∧ (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2 / x ⬝ᵥ x = r} (hL.eigenvalues i₀)

theorem CourantFischer.ones_ne_zero {V : Type u_1} [Nonempty V] : (fun (x : V) => 1) ≠ 0

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

theorem CourantFischer.laplacian_rayleigh_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) (hx : x ≠ 0) : 0 ≤ x ⬝ᵥ (SimpleGraph.lapMatrix ℝ G).mulVec x / x ⬝ᵥ x

theorem CourantFischer.laplacian_rayleigh_ones_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (((fun (x : V) => 1) ⬝ᵥ (SimpleGraph.lapMatrix ℝ G).mulVec fun (x : V) => 1) / (fun (x : V) => 1) ⬝ᵥ fun (x : V) => 1) = 0

theorem CourantFischer.laplacian_rayleighQuotient_min_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] : IsLeast {r : ℝ | ∃ (x : V → ℝ), x ≠ 0 ∧ x ⬝ᵥ (SimpleGraph.lapMatrix ℝ G).mulVec x / x ⬝ᵥ x = r} 0

theorem CourantFischer.corollary24_rayleighQuotient {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (hL : (SimpleGraph.lapMatrix ℝ G).IsHermitian) (k : V) (hk : ∀ (x : V → ℝ), (∀ (j : V), hL.eigenvalues j < hL.eigenvalues k → (hL.eigenvectorBasis j).ofLp ⬝ᵥ x = 0) ↔ ∑ i : V, x i = 0) (i₀ : V) (hi₀ : ∀ (j : V), hL.eigenvalues j ≤ hL.eigenvalues i₀) : IsLeast {r : ℝ | ∃ (x : V → ℝ), x ≠ 0 ∧ x ⬝ᵥ (SimpleGraph.lapMatrix ℝ G).mulVec x / x ⬝ᵥ x = r} 0 ∧ IsLeast {r : ℝ | ∃ (x : V → ℝ), x ≠ 0 ∧ ∑ i : V, x i = 0 ∧ (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2 / x ⬝ᵥ x = r} (hL.eigenvalues k) ∧ IsGreatest {r : ℝ | ∃ (x : V → ℝ), x ≠ 0 ∧ (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2 / x ⬝ᵥ x = r} (hL.eigenvalues i₀)