Subpolynomial growth of the divisor-counting function

This module develops the analytic-number-theory input used by the BGS middle- and end-game union bounds. The public target is an eventual real power bound for Nat.divisors.card.

theorem BGS.NumberTheory.eventually_card_divisors_le_rpow {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑n.divisors.card ≤ ↑n ^ ε

The divisor-counting function is eventually bounded by every positive real power. The cast and Real.rpow formulation is designed for direct use in the real-valued union bounds for divisors of p - 1 and p + 1.

theorem BGS.NumberTheory.exists_threshold_card_divisors_le_rpow {ε : ℝ} (hε : 0 < ε) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ↑n.divisors.card ≤ ↑n ^ ε

Threshold form of eventually_card_divisors_le_rpow, convenient when a downstream argument already carries explicit lower bounds for p - 1 and p + 1.