noncomputable def LovaszSimonovits.sortedValues {n : ℕ} (ρ : Fin n → ℝ) : Fin n → ℝ

noncomputable def LovaszSimonovits.partialSum {n : ℕ} (w : Fin n → ℝ) (k : ℕ) : ℝ

noncomputable def LovaszSimonovits.lsCurve {n : ℕ} (ρ : Fin n → ℝ) (x : ℝ) : ℝ

def LovaszSimonovits.IsSortedDecreasing {n : ℕ} (w : Fin n → ℝ) : Prop

def LovaszSimonovits.LSCurveIsConcave {n : ℕ} (ρ : Fin n → ℝ) : Prop

def LovaszSimonovits.WeightedSumInequality {n : ℕ} (ρ : Fin n → ℝ) : Prop

def LovaszSimonovits.RandomWalkStepReal {n : ℕ} (ρ_prev ρ_curr : Fin n → ℝ) : Prop

theorem LovaszSimonovits.lsCurve_nonincreasing {n : ℕ} (ρ_prev ρ_curr : Fin n → ℝ) (hstep : RandomWalkStepReal ρ_prev ρ_curr) (hclaim8 : WeightedSumInequality ρ_prev) (x : ℝ) (hx0 : 0 ≤ x) (hxn : x ≤ ↑n) : lsCurve ρ_curr x ≤ lsCurve ρ_prev x

theorem LovaszSimonovits.all_one_of_sum_ge_n {n : ℕ} (c : Fin n → ℝ) (hc1 : ∀ (i : Fin n), c i ≤ 1) (hge : ↑n ≤ Finset.univ.sum c) (i : Fin n) : c i = 1

theorem LovaszSimonovits.antitone_weighted_sum_le {n : ℕ} (w c : Fin n → ℝ) (hw : Antitone w) (hc0 : ∀ (i : Fin n), 0 ≤ c i) (hc1 : ∀ (i : Fin n), c i ≤ 1) (k : Fin n) (frac : ℝ) (hsum : Finset.univ.sum c = ↑↑k + frac) : ∑ i : Fin n, c i * w i ≤ partialSum w ↑k + frac * w k

theorem LovaszSimonovits.claim8_weighted_sum_inequality {n : ℕ} (ρ : Fin n → ℝ) (hconc : LSCurveIsConcave ρ) : WeightedSumInequality ρ

theorem LovaszSimonovits.theorem10_distribution_evolution {n : ℕ} (ρ_prev ρ_curr : Fin n → ℝ) (φ : ℝ) (hφ : 0 ≤ φ) (hφ1 : φ ≤ 1 / 2) (hclaim8 : WeightedSumInequality ρ_prev) (hmono : ∀ (a b : ℝ), 0 ≤ a → a ≤ b → b ≤ ↑n → lsCurve ρ_prev a ≤ lsCurve ρ_prev b) (harc_lower : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑n / 2 → ∃ (c₁ : Fin n → ℝ) (c₂ : Fin n → ℝ), (∀ (i : Fin n), 0 ≤ c₁ i) ∧ (∀ (i : Fin n), c₁ i ≤ 1) ∧ (∀ (i : Fin n), 0 ≤ c₂ i) ∧ (∀ (i : Fin n), c₂ i ≤ 1) ∧ Finset.univ.sum c₁ ≤ x - 2 * φ * x ∧ Finset.univ.sum c₂ ≤ x + 2 * φ * x ∧ lsCurve ρ_curr x = 1 / 2 * ∑ i : Fin n, c₁ i * sortedValues ρ_prev i + 1 / 2 * ∑ i : Fin n, c₂ i * sortedValues ρ_prev i) (harc_upper : ∀ (x : ℝ), ↑n / 2 ≤ x → x ≤ ↑n → ∃ (c₁ : Fin n → ℝ) (c₂ : Fin n → ℝ), (∀ (i : Fin n), 0 ≤ c₁ i) ∧ (∀ (i : Fin n), c₁ i ≤ 1) ∧ (∀ (i : Fin n), 0 ≤ c₂ i) ∧ (∀ (i : Fin n), c₂ i ≤ 1) ∧ Finset.univ.sum c₁ ≤ x - 2 * φ * (↑n - x) ∧ Finset.univ.sum c₂ ≤ x + 2 * φ * (↑n - x) ∧ lsCurve ρ_curr x = 1 / 2 * ∑ i : Fin n, c₁ i * sortedValues ρ_prev i + 1 / 2 * ∑ i : Fin n, c₂ i * sortedValues ρ_prev i) : (∀ (x : ℝ), 0 ≤ x → x ≤ ↑n / 2 → lsCurve ρ_curr x ≤ 1 / 2 * (lsCurve ρ_prev (x - 2 * φ * x) + lsCurve ρ_prev (x + 2 * φ * x))) ∧ ∀ (x : ℝ), ↑n / 2 ≤ x → x ≤ ↑n → lsCurve ρ_curr x ≤ 1 / 2 * (lsCurve ρ_prev (x - 2 * φ * (↑n - x)) + lsCurve ρ_prev (x + 2 * φ * (↑n - x)))

noncomputable def LovaszSimonovits.lovaszSimonovitsBound (n : ℕ) (φ : ℝ) (t : ℕ) (x : ℝ) : ℝ

def LovaszSimonovits.SatisfiesEvolutionBound {n : ℕ} (ρ : ℕ → Fin n → ℝ) (φ : ℝ) : Prop

theorem LovaszSimonovits.midpoint_mono_pointwise {f g : ℝ → ℝ} {a b : ℝ} (hfa : f a ≤ g a) (hfb : f b ≤ g b) : 1 / 2 * (f a + f b) ≤ 1 / 2 * (g a + g b)

def LovaszSimonovits.MidpointBoundLower (n : ℕ) (φ : ℝ) : Prop

def LovaszSimonovits.MidpointBoundUpper (n : ℕ) (φ : ℝ) : Prop

theorem LovaszSimonovits.sqrt_one_sub_le (t : ℝ) (ht1 : t ≤ 1) : √(1 - t) ≤ 1 - t / 2

theorem LovaszSimonovits.sqrt_midpoint_bound (φ : ℝ) (hφ : 0 ≤ φ) (hφ1 : φ ≤ 1 / 2) : 1 / 2 * (√(1 - 2 * φ) + √(1 + 2 * φ)) ≤ 1 - φ ^ 2 / 2

theorem LovaszSimonovits.midpoint_bound_lower_proof (n : ℕ) (φ : ℝ) (hφ : 0 ≤ φ) (hφ1 : φ ≤ 1 / 2) (hn : 0 < n) : MidpointBoundLower n φ

theorem LovaszSimonovits.midpoint_bound_upper_proof (n : ℕ) (φ : ℝ) (hφ : 0 ≤ φ) (hφ1 : φ ≤ 1 / 2) (hn : 0 < n) : MidpointBoundUpper n φ

theorem LovaszSimonovits.lovasz_simonovits {n : ℕ} (ρ : ℕ → Fin n → ℝ) (φ : ℝ) (hφ : 0 ≤ φ) (hφ1 : φ ≤ 1 / 2) (hevol : SatisfiesEvolutionBound ρ φ) (hbase : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑n → lsCurve (ρ 0) x ≤ lovaszSimonovitsBound n φ 0 x) (hmid_lower : MidpointBoundLower n φ) (hmid_upper : MidpointBoundUpper n φ) (t : ℕ) (x : ℝ) : 0 ≤ x → x ≤ ↑n → lsCurve (ρ t) x ≤ lovaszSimonovitsBound n φ t x

theorem LovaszSimonovits.lovasz_simonovits_full {n : ℕ} (ρ : ℕ → Fin n → ℝ) (φ : ℝ) (hn : 0 < n) (hφ : 0 ≤ φ) (hφ1 : φ ≤ 1 / 2) (hevol : SatisfiesEvolutionBound ρ φ) (hbase : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑n → lsCurve (ρ 0) x ≤ lovaszSimonovitsBound n φ 0 x) (t : ℕ) (x : ℝ) : 0 ≤ x → x ≤ ↑n → lsCurve (ρ t) x ≤ lovaszSimonovitsBound n φ t x

theorem LovaszSimonovits.lovasz_simonovits_complement_bound {n : ℕ} (φ : ℝ) (t : ℕ) (I_t : ℝ → ℝ) (x : ℝ) (hn : 0 < n) (hLS_nx : I_t (↑n - x) ≤ lovaszSimonovitsBound n φ t (↑n - x)) (hcompl : I_t x + I_t (↑n - x) ≥ 1) : x / ↑n ≤ I_t x + min √x √(↑n - x) * (1 - φ ^ 2 / 2) ^ t

theorem LovaszSimonovits.corollary12 {n : ℕ} (φ : ℝ) (t : ℕ) (I_t : ℝ → ℝ) (x : ℝ) (_hx0 : 0 ≤ x) (_hxn : x ≤ ↑n) (hLS : I_t x ≤ lovaszSimonovitsBound n φ t x) (hLS_lower : x / ↑n ≤ I_t x + min √x √(↑n - x) * (1 - φ ^ 2 / 2) ^ t) : |I_t x - x / ↑n| ≤ min √x √(↑n - x) * (1 - φ ^ 2 / 2) ^ t

theorem LovaszSimonovits.corollary12_from_theorem11 {n : ℕ} (φ : ℝ) (t : ℕ) (I_t : ℝ → ℝ) (x : ℝ) (hx0 : 0 ≤ x) (hxn : x ≤ ↑n) (hn : 0 < n) (hLS : I_t x ≤ lovaszSimonovitsBound n φ t x) (hLS_nx : I_t (↑n - x) ≤ lovaszSimonovitsBound n φ t (↑n - x)) (hcompl : I_t x + I_t (↑n - x) ≥ 1) : |I_t x - x / ↑n| ≤ min √x √(↑n - x) * (1 - φ ^ 2 / 2) ^ t

theorem LovaszSimonovits.corollary12_vertex_set {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (n t : ℕ) (p_t : V → ℝ) (W : Finset V) (x : ℝ) (_hx_vol : x = ↑(G.volume W)) (_hn_vol : n = G.volume Finset.univ) (hx0 : 0 ≤ x) (hxn : x ≤ ↑n) (hn : 0 < n) (I_t : ℝ → ℝ) (hmass : W.sum p_t = I_t x) (hLS : I_t x ≤ lovaszSimonovitsBound n (↑G.conductance) t x) (hLS_nx : I_t (↑n - x) ≤ lovaszSimonovitsBound n (↑G.conductance) t (↑n - x)) (hcompl : I_t x + I_t (↑n - x) ≥ 1) : |W.sum p_t - x / ↑n| ≤ min √x √(↑n - x) * (1 - ↑G.conductance ^ 2 / 2) ^ t