noncomputable def PageRank.pageRankVec {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (s : Fin n → ℝ) : Fin n → ℝ

theorem PageRank.pageRankVec_fixed_point {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (s : Fin n → ℝ) (hW : IsUnit (1 - (1 - α) • W)) : pageRankVec α W s = α • s + (1 - α) • W.mulVec (pageRankVec α W s)

theorem PageRank.pageRankVec_unique {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (s : Fin n → ℝ) (hW : IsUnit (1 - (1 - α) • W)) (x : Fin n → ℝ) (hx : x = α • s + (1 - α) • W.mulVec x) : x = pageRankVec α W s

theorem PageRank.pageRankVec_comm_W {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (s : Fin n → ℝ) (hcomm : Commute W (1 - (1 - α) • W)⁻¹) : pageRankVec α W (W.mulVec s) = W.mulVec (pageRankVec α W s)

theorem PageRank.pageRankVec_comm_W_of_isUnit {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (s : Fin n → ℝ) (hW : IsUnit (1 - (1 - α) • W)) : pageRankVec α W (W.mulVec s) = W.mulVec (pageRankVec α W s)

theorem PageRank.pageRankVec_eq2 {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (s : Fin n → ℝ) (hW : IsUnit (1 - (1 - α) • W)) (hcomm : Commute W (1 - (1 - α) • W)⁻¹) : pageRankVec α W s = α • s + (1 - α) • pageRankVec α W (W.mulVec s)

theorem PageRank.pageRankVec_add {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (s₁ s₂ : Fin n → ℝ) : pageRankVec α W (s₁ + s₂) = pageRankVec α W s₁ + pageRankVec α W s₂

theorem PageRank.pageRankVec_smul {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (c : ℝ) (s : Fin n → ℝ) : pageRankVec α W (c • s) = c • pageRankVec α W s

theorem PageRank.pageRankVec_linear {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (c d : ℝ) (v w : Fin n → ℝ) : pageRankVec α W (c • v + d • w) = c • pageRankVec α W v + d • pageRankVec α W w

theorem PageRank.pageRankVec_sub {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (s₁ s₂ : Fin n → ℝ) : pageRankVec α W (s₁ - s₂) = pageRankVec α W s₁ - pageRankVec α W s₂

theorem PageRank.pageRankVec_invariant_preserved {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (s p r : Fin n → ℝ) (u : Fin n) (hW : IsUnit (1 - (1 - α) • W)) (hcomm : Commute W (1 - (1 - α) • W)⁻¹) (hinv : p = pageRankVec α W (s - r)) : have χ_u := Pi.single u 1; have p' := p + (α * r u) • χ_u; have r' := r - r u • χ_u + ((1 - α) * r u) • W.mulVec χ_u; p' = pageRankVec α W (s - r')

noncomputable def PageRank.l1norm {n : ℕ} (f : Fin n → ℝ) : ℝ

theorem PageRank.l1norm_add_le {n : ℕ} (f g : Fin n → ℝ) : l1norm (f + g) ≤ l1norm f + l1norm g

theorem PageRank.l1norm_smul {n : ℕ} (c : ℝ) (f : Fin n → ℝ) : l1norm (c • f) = |c| * l1norm f

theorem PageRank.sum_mul_pi_single {n : ℕ} (W : Matrix (Fin n) (Fin n) ℝ) (i u : Fin n) : ∑ x : Fin n, W i x * Pi.single u 1 x = W i u

theorem PageRank.l1norm_sub_single {n : ℕ} (r : Fin n → ℝ) (u : Fin n) (hr : ∀ (i : Fin n), 0 ≤ r i) : have χ_u := Pi.single u 1; l1norm (r - r u • χ_u) = l1norm r - r u

theorem PageRank.l1norm_mulVec_single_le {n : ℕ} (W : Matrix (Fin n) (Fin n) ℝ) (u : Fin n) (hW : W ∈ Matrix.colStochastic ℝ (Fin n)) : have χ_u := Pi.single u 1; l1norm (W.mulVec χ_u) ≤ 1

theorem PageRank.residual_decrease_bound {n : ℕ} (α : ℝ) (W : Matrix (Fin n) (Fin n) ℝ) (r : Fin n → ℝ) (u : Fin n) (hα : 0 < α) (hα1 : α < 1) (hW : W ∈ Matrix.colStochastic ℝ (Fin n)) (hr : ∀ (i : Fin n), 0 ≤ r i) : have χ_u := Pi.single u 1; have r' := r - r u • χ_u + ((1 - α) * r u) • W.mulVec χ_u; l1norm r' ≤ l1norm r - α * r u

noncomputable def PageRank.vol {n : ℕ} (d : Fin n → ℝ) (S : Finset (Fin n)) : ℝ

noncomputable def PageRank.vecSupp {n : ℕ} (f : Fin n → ℝ) : Finset (Fin n)

theorem PageRank.telescope_decrease {T : ℕ} (a : Fin (T + 1) → ℝ) (b : Fin T → ℝ) (h : ∀ (i : Fin T), a ⟨↑i + 1, ⋯⟩ ≤ a ⟨↑i, ⋯⟩ - b i) : a ⟨T, ⋯⟩ ≤ a ⟨0, ⋯⟩ - ∑ i : Fin T, b i

theorem PageRank.pageRank_iteration_bound {n : ℕ} (α ε : ℝ) (hα : 0 < α) (hε : 0 < ε) (T : ℕ) (d : Fin n → ℝ) (hd : ∀ (v : Fin n), 1 ≤ d v) (residual_norms : Fin (T + 1) → ℝ) (h_nonneg : ∀ (i : Fin (T + 1)), 0 ≤ residual_norms i) (vertices : Fin T → Fin n) (residual_vals : Fin T → ℝ) (h_select : ∀ (i : Fin T), ε * d (vertices i) ≤ residual_vals i) (h_decrease : ∀ (i : Fin T), residual_norms ⟨↑i + 1, ⋯⟩ ≤ residual_norms ⟨↑i, ⋯⟩ - α * residual_vals i) : ↑T * (α * ε) ≤ residual_norms ⟨0, ⋯⟩

theorem PageRank.pageRank_degree_sum_bound {n : ℕ} (α ε : ℝ) (hα : 0 < α) (T : ℕ) (d : Fin n → ℝ) (residual_norms : Fin (T + 1) → ℝ) (h_nonneg : ∀ (i : Fin (T + 1)), 0 ≤ residual_norms i) (vertices : Fin T → Fin n) (residual_vals : Fin T → ℝ) (h_select : ∀ (i : Fin T), ε * d (vertices i) ≤ residual_vals i) (h_decrease : ∀ (i : Fin T), residual_norms ⟨↑i + 1, ⋯⟩ ≤ residual_norms ⟨↑i, ⋯⟩ - α * residual_vals i) : α * ε * ∑ i : Fin T, d (vertices i) ≤ residual_norms ⟨0, ⋯⟩

theorem PageRank.vol_supp_le_degree_sum {n : ℕ} (d : Fin n → ℝ) (hd : ∀ (v : Fin n), 0 ≤ d v) (p : Fin n → ℝ) (T : ℕ) (vertices : Fin T → Fin n) (h_supp_covered : ∀ v ∈ vecSupp p, ∃ (i : Fin T), vertices i = v) : vol d (vecSupp p) ≤ ∑ i : Fin T, d (vertices i)

theorem PageRank.pageRank_output_quality {n : ℕ} (ε : ℝ) (d r : Fin n → ℝ) (hd_pos : ∀ (v : Fin n), 0 < d v) (h_term : ∀ (v : Fin n), r v < ε * d v) (v : Fin n) : r v / d v < ε

theorem PageRank.pageRank_termination {n : ℕ} (α ε : ℝ) (hα : 0 < α) (hε : 0 < ε) (T : ℕ) (d : Fin n → ℝ) (hd : ∀ (v : Fin n), 1 ≤ d v) (p r_final : Fin n → ℝ) (residual_norms : Fin (T + 1) → ℝ) (h_init : residual_norms ⟨0, ⋯⟩ = 1) (h_nonneg : ∀ (i : Fin (T + 1)), 0 ≤ residual_norms i) (vertices : Fin T → Fin n) (residual_vals : Fin T → ℝ) (h_select : ∀ (i : Fin T), ε * d (vertices i) ≤ residual_vals i) (h_decrease : ∀ (i : Fin T), residual_norms ⟨↑i + 1, ⋯⟩ ≤ residual_norms ⟨↑i, ⋯⟩ - α * residual_vals i) (h_term : ∀ (v : Fin n), r_final v < ε * d v) (h_supp_covered : ∀ v ∈ vecSupp p, ∃ (i : Fin T), vertices i = v) : ↑T * (α * ε) ≤ 1 ∧ (∀ (v : Fin n), r_final v / d v < ε) ∧ α * ε * vol d (vecSupp p) ≤ 1