Fixed-order divisor coefficients are subpolynomial

The proved moment estimate, with an arbitrarily large fixed moment, pays every positive power. No divisor bound is assumed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.eventually_fouvryTau_le_rpow {k : ℕ} (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑((fouvryTau k) n) ≤ ↑n ^ ε

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_le_const_rpow {k : ℕ} (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 0 < n → ↑((fouvryTau k) n) ≤ C * ↑n ^ ε

The constant depends only on the fixed order and exponent.