noncomputable def RandomWalks.stationaryDist {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : ℝ

theorem RandomWalks.stationaryDist_sum_eq_one {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hpos : 0 < ∑ u : V, ↑(G.degree u)) : ∑ v : V, stationaryDist G v = 1

noncomputable def RandomWalks.walkMatrix {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Matrix V V ℝ

noncomputable def RandomWalks.stationaryVec {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : V → ℝ

theorem RandomWalks.adjMatrix_row_sum {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : V) : ∑ i : V, SimpleGraph.adjMatrix ℝ G k i = ↑(G.degree k)

theorem RandomWalks.degree_pos_of_adj {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {k x : V} (h : G.Adj k x) : 0 < G.degree x

theorem RandomWalks.walkMatrix_stationaryVec_term {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (k x : V) (S : ℝ) : SimpleGraph.adjMatrix ℝ G k x / ↑(G.degree x) * (↑(G.degree x) / S) = SimpleGraph.adjMatrix ℝ G k x / S

theorem RandomWalks.walkMatrix_mulVec_stationaryVec {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : (walkMatrix G).mulVec (stationaryVec G) = stationaryVec G

theorem RandomWalks.eigenspace_conj_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (e : M ≃ₗ[R] M) (f : Module.End R M) (μ : R) : (e.conj f).eigenspace μ = Submodule.map (↑e) (f.eigenspace μ)

theorem RandomWalks.hasEigenvalue_conj_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (e : M ≃ₗ[R] M) (f : Module.End R M) (μ : R) : (e.conj f).HasEigenvalue μ ↔ f.HasEigenvalue μ

noncomputable def RandomWalks.rwMatrixGen {V : Type u_3} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Matrix V V ℝ

noncomputable def RandomWalks.normWalkMatrix {V : Type u_3} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Matrix V V ℝ

theorem RandomWalks.normWalkMatrix_eq_conj_rwMatrixGen {V : Type u_3} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : normWalkMatrix G = (Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹) * rwMatrixGen G * Matrix.diagonal fun (v : V) => √↑(G.degree v)

noncomputable def RandomWalks.lazyRwMatrixGen {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Matrix V V ℝ

noncomputable def RandomWalks.normLazyWalkMatrix {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Matrix V V ℝ

noncomputable def RandomWalks.lazyRwMatrix {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) : Matrix V V ℝ

theorem RandomWalks.adjMatrix_isHermitian {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] : (SimpleGraph.adjMatrix ℝ G).IsHermitian

theorem RandomWalks.normLazyWalkMatrix_isHermitian {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] : (normLazyWalkMatrix G).IsHermitian

noncomputable def RandomWalks.l2Norm {V : Type u_1} [Fintype V] (f : V → ℝ) : ℝ

noncomputable def RandomWalks.l2Dist {V : Type u_1} [Fintype V] (p q : V → ℝ) : ℝ

theorem RandomWalks.lazy_rw_convergence_bound {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (p₀ : V → ℝ) (μ₂' : ℝ) (hμ₂'_nn : 0 ≤ μ₂') (hμ₂'_lt : μ₂' < 1) (t : ℕ) : (l2Dist ((lazyRwMatrixGen G ^ t).mulVec p₀) fun (v : V) => ↑(G.degree v) / ∑ u : V, ↑(G.degree u)) ≤ μ₂' ^ t * √((Finset.univ.sup' ⋯ fun (v : V) => ↑(G.degree v)) / Finset.univ.inf' ⋯ fun (v : V) => ↑(G.degree v))

theorem RandomWalks.lazy_rw_pointwise_convergence {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (hpos : ∀ (v : V), 0 < G.degree v) (μ₂' : ℝ) (hμ₂'_nn : 0 ≤ μ₂') (hμ₂'_lt : μ₂' < 1) (h_spectral_bound : ∀ (i : V), ⋯.eigenvalues i ≤ μ₂' ∨ ⋯.eigenvalues i = 1) (p₀ : V → ℝ) (hp_sum : ∑ v : V, p₀ v = 1) (hp_nn : ∀ (v : V), 0 ≤ p₀ v) (t : ℕ) (v : V) : |(lazyRwMatrixGen G ^ t).mulVec p₀ v - ↑(G.degree v) / ∑ u : V, ↑(G.degree u)| ≤ μ₂' ^ t * √(↑(G.degree v) / Finset.univ.inf' ⋯ fun (y : V) => ↑(G.degree y))

theorem RandomWalks.sqrtDeg_mul_sqrtDeg_inv {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hpos : ∀ (v : V), 0 < G.degree v) : ((Matrix.diagonal fun (v : V) => √↑(G.degree v)) * Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹) = 1

theorem RandomWalks.sqrtDeg_inv_mul_sqrtDeg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hpos : ∀ (v : V), 0 < G.degree v) : ((Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹) * Matrix.diagonal fun (v : V) => √↑(G.degree v)) = 1

noncomputable def RandomWalks.sqrtDegEquiv {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hpos : ∀ (v : V), 0 < G.degree v) : (V → ℝ) ≃ₗ[ℝ] V → ℝ

theorem RandomWalks.rwMatrixGen_eq_sqrt_mul_normWalkMatrix_mul_sqrt_inv {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hpos : ∀ (v : V), 0 < G.degree v) : rwMatrixGen G = (Matrix.diagonal fun (v : V) => √↑(G.degree v)) * normWalkMatrix G * Matrix.diagonal fun (v : V) => (√↑(G.degree v))⁻¹

theorem RandomWalks.rwMatrixGen_eq_conj_normWalkMatrix {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hpos : ∀ (v : V), 0 < G.degree v) : Matrix.toLin' (rwMatrixGen G) = (sqrtDegEquiv G hpos).conj (Matrix.toLin' (normWalkMatrix G))

theorem RandomWalks.normWalkMatrix_rwMatrixGen_same_eigenvalues {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hpos : ∀ (v : V), 0 < G.degree v) (μ : ℝ) : Module.End.HasEigenvalue (Matrix.toLin' (normWalkMatrix G)) μ ↔ Module.End.HasEigenvalue (Matrix.toLin' (rwMatrixGen G)) μ

theorem RandomWalks.hasEigenvalue_conj_graph_iff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hpos : ∀ (v : V), 0 < G.degree v) (μ : ℝ) : Module.End.HasEigenvalue (Matrix.toLin' (rwMatrixGen G)) μ ↔ Module.End.HasEigenvalue (Matrix.toLin' (normWalkMatrix G)) μ

theorem RandomWalks.expander_matching_contraction_ratio {L : Type u_1} {R : Type u_2} [Fintype L] [Fintype R] [DecidableEq L] [DecidableEq R] (G : SimpleGraph (L ⊕ R)) [DecidableRel G.Adj] {d : ℕ} {α β : ℝ} (hbip : G.IsBipartiteOn) (hreg : G.IsRegularOfDegree d) (hexp : G.IsBipartiteExpander α β) (hd : 0 < ↑d) (Si : Finset L) (hSi : ↑Si.card ≤ α * ↑(Fintype.card L)) (hSi_pos : 0 < ↑Si.card) (Si1_card : ℝ) (hSi1 : Si1_card ≤ ↑Si.card - ↑(G.uniqueNeighbors Si).card / ↑d) : Si1_card / ↑Si.card ≤ 2 * (1 - β / ↑d)

theorem SimpleGraph.rw_convergence_conductance_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected) (S : Finset V) (t : ℕ) (p₀ : V → ℝ) (m : ℕ) (hm : m = G.edgeFinset.card) (x : ℝ) (hx : x = ∑ w ∈ S, ↑(G.degree w)) (φ : ℝ) (hφ : φ = ↑(G.setConductance S)) : |∑ w ∈ S, ((RandomWalks.lazyRwMatrixGen G ^ t).mulVec p₀ w - RandomWalks.stationaryDist G w)| ≤ min √x √(2 * ↑m - x) * (1 - φ ^ 2 / 2) ^ t