Asymptotics of the pairing and entropy inequality

A sublinear logarithmic rectangle threshold makes the designated-pair survival fraction tend to one. The finite inequality therefore retains the full constant gateCoefficient, rather than only a fixed weaker rational coefficient.

theorem Algebraic.Cutwidth.Aggregate.Geometry.clog_isLittleO {K : ℕ → ℕ} (small : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ K n) : (fun (n : ℕ) => ↑(Nat.clog 2 (K n))) =o[Filter.atTop] fun (n : ℕ) => ↑n

Rounding a sublinear positive logarithmic threshold preserves sublinearity.

theorem Algebraic.Cutwidth.Aggregate.Geometry.eventually_threshold_range {k : ℕ → ℕ} (small : (fun (n : ℕ) => ↑(k n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) : ∀ᶠ (n : ℕ) in Filter.atTop, k n + 3 ≤ n

Eventually a sublinear nonnegative threshold leaves at least two sending coordinates.

theorem Algebraic.Cutwidth.Aggregate.Geometry.pairRetention_tendsto {k : ℕ → ℕ} (small : (fun (n : ℕ) => ↑(k n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) : Filter.Tendsto (fun (n : ℕ) => pairRetention n (k n)) Filter.atTop (nhds 1)

A sublinear receiving side preserves almost every designated pair.

theorem Algebraic.Cutwidth.Aggregate.Geometry.normalized_bound_tendsto {K : ℕ → ℕ} (small : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ K n) : Filter.Tendsto (fun (n : ℕ) => (1 + 2 * (Entropy.bitSaving * pairRetention n (Nat.clog 2 (K n))) - 2 * (Entropy.bitSaving * pairRetention n (Nat.clog 2 (K n))) * (↑(Nat.clog 2 (K n)) / ↑n) - (↑(Nat.clog 2 (K n)) / ↑n + 2 / ↑n) - Real.logb 2 ↑(K n) / ↑n) / (1 + Entropy.bitSaving * pairRetention n (Nat.clog 2 (K n)))) Filter.atTop (nhds gateCoefficient)

The normalized finite lower bound tends to the full pairing/entropy coefficient.

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

Absorb the finite geometric and logarithmic losses in arbitrary positive linear slack.