Absorbing the one-way capacity remainder

A capacity bound with twice the logarithmic rectangle threshold and a constant remainder gives a leading coefficient of one when the threshold has sublinear logarithm.

theorem Algebraic.Cutwidth.Aggregate.eventually_lt_of_real_oneWayBound (K : ℕ → ℕ) (small : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ K n) (C : ℕ) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (B : ℝ), ↑n ≤ B + 2 * ↑(Nat.clog 2 (K n)) + ↑C → (1 - ε) * ↑n < B

A sublinear rectangle threshold absorbs the finite one-way counting remainder.

theorem Algebraic.Cutwidth.Aggregate.eventually_lt_of_oneWayBound (K : ℕ → ℕ) (small : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ K n) (C : ℕ) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (B : ℕ), n ≤ B + 2 * Nat.clog 2 (K n) + C → (1 - ε) * ↑n < ↑B

The integer-capacity specialization of the one-way remainder estimate.