Exponential error below the frontier size threshold

theorem Complexity.Frontier.eventually_frontier_log_error {A ε γ : ℝ} (hA : 0 < A) (hε : 0 < ε) (hγ1 : γ < 1) (hγε : γ < A * ε) (K : ℕ → ℕ) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) : ∃ η > 0, ∀ (C : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, 1 + 2 * Real.logb 2 ↑(K n) ≤ (1 - γ) * ↑n ∧ ∀ (s v w : ℝ), 0 ≤ s → 0 ≤ v → s ≤ (1 + 1 / A - ε) * ↑n → v ≤ 4 * s + 3 → w ≤ (A + η) * (s - ↑n + Real.logb 2 ↑(K n) + 1) + η * v + C → w + 4 + 3 * Real.logb 2 ↑(K n) + Real.logb 2 (v + 1) ≤ (1 - γ) * ↑n

Below (1 + 1/A - ε)n, frontier counts have an exponential margin. The independent condition γ < 1 also absorbs the small output classes when many inputs are unused.

theorem Complexity.Frontier.div_two_pow_le_of_logb {x γ : ℝ} {n : ℕ} (hx : 0 < x) (h : Real.logb 2 x ≤ (1 - γ) * ↑n) : x / 2 ^ n ≤ 2 ^ (-γ * ↑n)

A logarithmic count bound becomes an exponentially small fraction of all Boolean inputs.