Asymptotics of shared-control and refined message counting #
A sublinear receiving side retains almost every designated triple. All finite threshold losses vanish after normalization, leaving the stronger full coefficient.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Shared.receiverRetention_tendsto
{k : ℕ → ℕ}
(small : (fun (n : ℕ) => ↑(k n)) =o[Filter.atTop] fun (n : ℕ) => ↑n)
:
Filter.Tendsto (fun (n : ℕ) => receiverRetention n (k n)) Filter.atTop (nhds 1)
A sublinear receiving side preserves asymptotically every selected primary triple.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Shared.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 - Joint.overlapPenalty) * (1 - ↑(Nat.clog 2 (K n)) / ↑n - 1 / ↑n) + receiverRetention n (Nat.clog 2 (K n)) * (Joint.gateSaving / 2 + 3 * wideSaving / 2) - 2 * receiverRetention n (Nat.clog 2 (K n)) * wideSaving * (↑(Nat.clog 2 (K n)) / ↑n) - 1 / ↑n - Real.logb 2 ↑(K n) / ↑n) / (1 + receiverRetention n (Nat.clog 2 (K n)) * wideSaving))
Filter.atTop (nhds gateCoefficient)
The normalized finite shared-control bound converges to its exact gate coefficient.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Shared.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 + receiverRetention n (Nat.clog 2 (K n)) * wideSaving) * g ≥ (1 - Joint.overlapPenalty) * (↑n - ↑(Nat.clog 2 (K n)) - 1) + receiverRetention n (Nat.clog 2 (K n)) * (Joint.gateSaving / 2 + 3 * wideSaving / 2) * ↑n - 2 * receiverRetention n (Nat.clog 2 (K n)) * wideSaving * ↑(Nat.clog 2 (K n)) - 1 - Real.logb 2 ↑(K n) →
(gateCoefficient - ε) * ↑n < g
Absorb every finite logarithmic loss into an arbitrary positive linear slack.