Absorbing the logarithmic initial deficit

The middle-layer deficit bound is little-o of every positive power of n. Thus replacing the parity deficit 1 with this logarithmic bound preserves the exponent 1/(d-1) in a d-round communication lower bound.

theorem Complexity.BooleanAnalysis.majorityDeficitBound_eventually_le_internal {r c : ℝ} (hr : 0 < r) (hc : 0 < c) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → majorityDeficitBound n ≤ c * ↑n ^ r

theorem Complexity.KarchmerWigderson.finite_budget_with_deficit_of_cost_internal {n d : ℕ} (hd : 0 < d) {m k : ℝ} (hm : 0 ≤ m) (hk : 0 ≤ k) (hcost : m ≤ ↑n ^ (↑d)⁻¹ / (128 * (32768 * 194 ^ d))) (hkcost : k ≤ ↑n ^ (↑d)⁻¹ / (128 * (32768 * 194 ^ d))) : 64 * (32768 * 194 ^ d * (m + k)) ^ d ≤ ↑n