@[reducible, inline]

abbrev Expanders.IsDRegular {V : Type u_1} (G : SimpleGraph V) [G.LocallyFinite] (d : ℕ) : Prop

noncomputable def Expanders.indicatorVec {V : Type u_1} [DecidableEq V] (S : Finset V) : V → ℝ

def SimpleGraph.setNeighborFinset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset V

def SimpleGraph.IsVertexExpander {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (α β : ℝ) : Prop

noncomputable def SimpleGraph.edgeCountBetween {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (S T : Finset V) : ℕ

noncomputable def SimpleGraph.adjEigenvalues {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Fin (Fintype.card V) → ℝ

noncomputable def SimpleGraph.secondLargestAdjEigenvalue {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hcard : Fintype.card V ≥ 2) : ℝ

theorem SimpleGraph.expander_mixing_lemma {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (hd : G.IsRegularOfDegree d) (hcard : Fintype.card V ≥ 2) (S T : Finset V) : |↑(G.edgeCountBetween S T) - ↑d * ↑S.card * ↑T.card / ↑(Fintype.card V)| ≤ G.secondLargestAdjEigenvalue hcard / ↑(Fintype.card V) * √(↑S.card * ↑(Fintype.card V - S.card) * (↑T.card * ↑(Fintype.card V - T.card)))

theorem SimpleGraph.expander_vertex_expansion_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (hd : G.IsRegularOfDegree d) (hcard : Fintype.card V ≥ 2) (hd_pos : ↑d > 0) (X : Finset V) (hX : X.Nonempty) (hmu : G.secondLargestAdjEigenvalue hcard ^ 2 + (↑d ^ 2 - G.secondLargestAdjEigenvalue hcard ^ 2) * ↑X.card / ↑(Fintype.card V) > 0) : ↑(G.setNeighborFinset X).card ≥ ↑d ^ 2 * ↑X.card / (G.secondLargestAdjEigenvalue hcard ^ 2 + (↑d ^ 2 - G.secondLargestAdjEigenvalue hcard ^ 2) * ↑X.card / ↑(Fintype.card V))

noncomputable def BipartiteMatching.partialMatchingsOfSize (n : ℕ) (adj : Fin n → Fin n → Bool) (k : ℕ) : Finset (Finset (Fin n × Fin n))

def BipartiteMatching.HasMinDegree (n : ℕ) (adj : Fin n → Fin n → Bool) (d : ℕ) : Prop

theorem BipartiteMatching.matching_ratio_bound (n : ℕ) (hn : 0 < n) (adj : Fin n → Fin n → Bool) (hdeg : HasMinDegree n adj ((n + 1) / 2)) (k : ℕ) (hk : 1 ≤ k) (hk' : k ≤ n) : (partialMatchingsOfSize n adj k).card ≤ n ^ 2 * (partialMatchingsOfSize n adj (k - 1)).card ∧ (partialMatchingsOfSize n adj (k - 1)).card ≤ n ^ 2 * (partialMatchingsOfSize n adj k).card

structure SpectralExpanders.GraphFamily : Type (u_1 + 1)

• V : ℕ → Type u_1
• instFintype (n : ℕ) : Fintype (self.V n)
• instDecidableEq (n : ℕ) : DecidableEq (self.V n)
• G (n : ℕ) : SimpleGraph (self.V n)
• instDecidableAdj (n : ℕ) : DecidableRel (self.G n).Adj
• d : ℕ
• isRegular (n : ℕ) : (self.G n).IsRegularOfDegree self.d
• card_ge_two (n : ℕ) : Fintype.card (self.V n) ≥ 2

noncomputable def SpectralExpanders.GraphFamily.setConductanceAt (F : GraphFamily) (n : ℕ) (S : Finset (F.V n)) : ℝ

noncomputable def SpectralExpanders.GraphFamily.familyConductance (F : GraphFamily) (n : ℕ) : ℝ

def SpectralExpanders.IsExpanderFamilyConductance (F : GraphFamily) : Prop

def SimpleGraph.bipartiteNeighborFinset {L : Type u_1} {R : Type u_2} [Fintype R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] (S : Finset L) : Finset R

def SimpleGraph.IsBipartiteExpander {L : Type u_1} {R : Type u_2} [Fintype L] [Fintype R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] (α β : ℝ) : Prop

theorem ExpanderDiameter.smul_matrix_pow {V : Type u_1} [Fintype V] [DecidableEq V] (c : ℝ) (A : Matrix V V ℝ) (n : ℕ) : (c • A) ^ n = c ^ n • A ^ n

theorem ExpanderDiameter.polynomial_diameter_bound {V : Type u_1} [Fintype V] [DecidableEq V] {d : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] (_hG : G.IsRegularOfDegree d) (_hd : 0 < d) (p : Polynomial ℝ) {k : ℕ} (hp : p.natDegree ≤ k) (M : Matrix V V ℝ) (hM : M = (1 / ↑d) • SimpleGraph.adjMatrix ℝ G) (h_pos : ∀ (u v : V), 0 < (Polynomial.aeval M) p u v) : G.diam ≤ k

theorem ExpanderDiameter.aeval_matrix_diagonal {m : Type u_2} [Fintype m] [DecidableEq m] (v : m → ℝ) (p : Polynomial ℝ) : (Polynomial.aeval (Matrix.diagonal v)) p = Matrix.diagonal fun (i : m) => Polynomial.eval (v i) p

theorem ExpanderDiameter.aeval_conjStarAlgAut_eq {m : Type u_2} [Fintype m] [DecidableEq m] (u : ↥(Matrix.unitaryGroup m ℝ)) (D : Matrix m m ℝ) (p : Polynomial ℝ) : (Polynomial.aeval (((Unitary.conjStarAlgAut ℝ (Matrix m m ℝ)) u) D)) p = ((Unitary.conjStarAlgAut ℝ (Matrix m m ℝ)) u) ((Polynomial.aeval D) p)

theorem ExpanderDiameter.conjStarAlgAut_diagonal_entry_eq {m : Type u_2} [Fintype m] [DecidableEq m] (u : ↥(Matrix.unitaryGroup m ℝ)) (d : m → ℝ) (a b : m) : ((Unitary.conjStarAlgAut ℝ (Matrix m m ℝ)) u) (Matrix.diagonal d) a b = ∑ i : m, d i * ↑u a i * ↑u b i

theorem ExpanderDiameter.aeval_hermitian_entry {m : Type u_2} [Fintype m] [DecidableEq m] (M : Matrix m m ℝ) (hM : M.IsHermitian) (p : Polynomial ℝ) (a b : m) : (Polynomial.aeval M) p a b = ∑ i : m, Polynomial.eval (hM.eigenvalues i) p * ↑hM.eigenvectorUnitary a i * ↑hM.eigenvectorUnitary b i

theorem ExpanderDiameter.unitary_row_sq_sum_eq_one {m : Type u_2} [Fintype m] [DecidableEq m] (u : ↥(Matrix.unitaryGroup m ℝ)) (a : m) : ∑ k : m, ↑u a k ^ 2 = 1

theorem ExpanderDiameter.walk_matrix_mulVec_ones {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] {d : ℕ} (hd : 0 < d) (hreg : G.IsRegularOfDegree d) (M : Matrix (Fin n) (Fin n) ℝ) (hM : M = (1 / ↑d) • SimpleGraph.adjMatrix ℝ G) : M.mulVec (Function.const (Fin n) 1) = Function.const (Fin n) 1

theorem ExpanderDiameter.walk_matrix_eigenvalues₀_zero_eq_one {n : ℕ} (hn : 0 < n) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] {d : ℕ} (hd : 0 < d) (hreg : G.IsRegularOfDegree d) (M : Matrix (Fin n) (Fin n) ℝ) (hM : M = (1 / ↑d) • SimpleGraph.adjMatrix ℝ G) (hM_sym : M.IsHermitian) : hM_sym.eigenvalues₀ ⟨0, ⋯⟩ = 1

theorem ExpanderDiameter.poly_degree_bounds_diameter {n : ℕ} (hn : 0 < n) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] {d : ℕ} (hd : 0 < d) (hreg : G.IsRegularOfDegree d) (M : Matrix (Fin n) (Fin n) ℝ) (hM : M = (1 / ↑d) • SimpleGraph.adjMatrix ℝ G) (hM_sym : M.IsHermitian) (p : Polynomial ℝ) (k : ℕ) (hp_deg : p.natDegree ≤ k) (hp_one : Polynomial.eval 1 p = 1) (hp_small : ∀ (i : Fin (Fintype.card (Fin n))), ↑i ≥ 1 → |Polynomial.eval (hM_sym.eigenvalues₀ i) p| < 1 / ↑n) : G.diam ≤ k

theorem ExpanderDiameter.one_sub_lt_exp_neg_of_pos {lam : ℝ} (hlam_pos : 0 < lam) : 1 - lam < Real.exp (-lam)

theorem ExpanderDiameter.spectral_gap_rpow_bound {lam : ℝ} (hlam_pos : 0 < lam) (hlam_le : lam ≤ 1) {n : ℕ} (hn : 2 ≤ n) : (1 - lam) ^ (Real.log ↑n / lam) < 1 / ↑n

theorem ExpanderDiameter.spectral_gap_nat_pow_bound {lam : ℝ} (hlam_pos : 0 < lam) (hlam_le : lam ≤ 1) {n : ℕ} (hn : 2 ≤ n) : (1 - lam) ^ ⌈Real.log ↑n / lam⌉₊ < 1 / ↑n

theorem ExpanderDiameter.diameter_spectral_gap_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (_hd : 0 < d) (_hreg : G.IsRegularOfDegree d) (hcard : Fintype.card V ≥ 2) (μ₂ : ℝ) (_hμ₂_nonneg : 0 ≤ μ₂) (hμ₂_lt : μ₂ < 1) (hpointwise : ∀ (u v : V) (t : ℕ), |((2⁻¹ • (1 + (↑d)⁻¹ • SimpleGraph.adjMatrix ℝ G)) ^ t) u v - 1 / ↑(Fintype.card V)| ≤ μ₂ ^ t) : G.diam ≤ ⌈Real.log ↑(Fintype.card V) / (1 - μ₂)⌉₊

theorem MagicPolynomial.magic_chebyshev_polynomial (t : ℝ) (ht0 : 0 < t) (ht1 : t < 1) (k : ℕ) : ∃ (p : Polynomial ℝ), p.natDegree = k ∧ Polynomial.eval 1 p = 1 ∧ ∀ (x : ℝ), 0 ≤ x → x ≤ 1 - t → |Polynomial.eval x p| ≤ 2 * (1 + √(2 * t))⁻¹ ^ k

@[reducible, inline]

noncomputable abbrev SimpleGraph.diameter {V : Type u_1} (G : SimpleGraph V) : ℕ