Parameters for square-root-sized supports

For a fixed accuracy parameter, split off a fixed fraction of the logarithm of the support size. Every secondary table then has an exponential margin. The arithmetic is over natural numbers; the final real epsilon enters only in the public asymptotic statements.

theorem Complexity.CircuitSparseSynthesis.Internal.eventually_polynomial_le_pow_div (constant degree divisor : ℕ) (positive : 0 < divisor) : ∀ᶠ (p : ℕ) in Filter.atTop, constant * p ^ degree ≤ 2 ^ (p / divisor)

theorem Complexity.CircuitSparseSynthesis.Internal.parameter_bounds (q p h : ℕ) (qbig : 32 ≤ q) (hbig : 2 * q ≤ h) (lower : q ^ 2 * h ≤ p) (upper : p < q ^ 2 * (h + 1)) : have k := (q + 1) * h; have l := p - h; have K := q - 2; have J := (q ^ 2 - 6 * q - 6) * h; have a := q * h; have steps := q + 1; h ≤ p ∧ 0 < K ∧ 0 < J ∧ k + l = p + a ∧ k + l ≤ 2 * p ∧ k ≤ p - h ∧ l ≤ p - h ∧ (k + 1) * K ≤ p - h ∧ 4 * k + 6 + J ≤ p - h ∧ K ≤ p ∧ steps ≤ p + 1 ∧ p + h ≤ a * steps ∧ p + h ≤ k + l

theorem Complexity.CircuitSparseSynthesis.Internal.parameter_main (P p h : ℕ) (hbig : 2 * (32 * (P + 1)) ≤ h) (upper : p < (32 * (P + 1)) ^ 2 * (h + 1)) : have q := 32 * (P + 1); 2 * P * (q + 1) ≤ (2 * P + 1) * (q - 2) ∧ 2 * P * p ≤ (2 * P + 1) * ((q ^ 2 - 6 * q - 6) * h)

theorem Complexity.CircuitSparseSynthesis.Internal.scaled_div_le {coefficient limit divisor value : ℕ} (positive : 0 < divisor) (bound : coefficient ≤ limit * divisor) : coefficient * (value / divisor) ≤ limit * value

theorem Complexity.CircuitSparseSynthesis.Internal.eventually_parameters (P : ℕ) : ∀ᶠ (p : ℕ) in Filter.atTop, ∃ (k : ℕ) (l : ℕ) (K : ℕ) (J : ℕ) (a : ℕ) (steps : ℕ), 0 < K ∧ 0 < J ∧ k + l = p + a ∧ P * sparseFiniteBudget (2 * p) k l K p a steps ≤ (P + 1) * 2 ^ p ∧ P * p * partialFiniteBudget (2 * p) k l J (2 ^ p) ≤ (P + 1) * 2 ^ p