Asymptotics of joint conjunction-message counting

The receiver keeps a sublinear number of inputs. Pair retention tends to one, and the finite variable charge retains the full joint-entropy coefficient.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.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 - overlapPenalty + 2 * (gateSaving * pairRetention n (Nat.clog 2 (K n))) - 2 * (gateSaving * pairRetention n (Nat.clog 2 (K n))) * (↑(Nat.clog 2 (K n)) / ↑n) - (1 - overlapPenalty) * (↑(Nat.clog 2 (K n)) / ↑n + 1 / ↑n) - 1 / ↑n - Real.logb 2 ↑(K n) / ↑n) / (1 + gateSaving * pairRetention n (Nat.clog 2 (K n)))) Filter.atTop (nhds gateCoefficient)

The normalized joint-message inequality tends to its exact coefficient.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.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 + gateSaving * pairRetention n (Nat.clog 2 (K n))) * g ≥ (1 - overlapPenalty + 2 * (gateSaving * pairRetention n (Nat.clog 2 (K n)))) * ↑n - 2 * (gateSaving * pairRetention n (Nat.clog 2 (K n))) * ↑(Nat.clog 2 (K n)) - (1 - overlapPenalty) * (↑(Nat.clog 2 (K n)) + 1) - 1 - Real.logb 2 ↑(K n) → (gateCoefficient - ε) * ↑n < g

Finite losses vanish for every sublinear logarithmic sumset threshold.