Sparsification -- choosing the parameter

The number of leaves is at most ∑_{j ≤ ρ} (Λ choose j) ≤ exp (Λ / T) T ^ ρ for every T ≥ 1 (sum_choose_le_exp_mul_pow), with Λ = N k X ^ (2 k) and α ρ ≤ (k - 1) N. Take T = M k X ^ (2 k) with 1/M ≤ (ε/2) log 2, so that exp (Λ / T) ≤ 2 ^ (ε N / 2). Since T is a polynomial in α, for α large T ^ (k - 1) ≤ 2 ^ (ε α / 2), hence T ^ ρ ≤ 2 ^ (ε N / 2).

theorem Complexity.ClauseSet.Sparsify.sum_choose_le_exp_mul_pow (Λ ρ T : ℕ) (hT : 1 ≤ T) : ∑ j ∈ Finset.range (ρ + 1), ↑(Λ.choose j) ≤ Real.exp (↑Λ / ↑T) * ↑T ^ ρ

A binomial tail bound. For every T ≥ 1, ∑_{j ≤ ρ} (Λ choose j) ≤ exp (Λ / T) T ^ ρ.

theorem Complexity.ClauseSet.Sparsify.exists_mul_pow_le_pow (C : ℝ) (d : ℕ) {r : ℝ} (hr : 1 < r) : ∃ (α : ℕ), 1 ≤ α ∧ C * ↑α ^ d ≤ r ^ α

A polynomial is eventually below an exponential with base r > 1.

theorem Complexity.ClauseSet.Sparsify.exists_sparsification (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (c : ℕ), ∀ (N : ℕ) (φ : ClauseSet N), (∀ C ∈ φ, C.card ≤ k) → ∃ (Ψ : Finset (ClauseSet N)), ↑Ψ.card ≤ 2 ^ (ε * ↑N) ∧ (∀ ψ ∈ Ψ, (∀ C ∈ ψ, C.card ≤ k) ∧ (∀ (v : Fin N), ψ.occurrences v ≤ c) ∧ ψ.solutions ⊆ φ.solutions) ∧ φ.solutions ⊆ Ψ.biUnion solutions

The sparsification lemma, internal form.