Small-power bounds for logarithms, divisor counts and completed moduli.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_log {δ x H : ℝ} (hδ : 0 < δ) (hx : 1 ≤ x) (hH : 0 < H) (hHx : H ≤ 8 * x ^ 6) : 1 + Real.log (2 * H) ≤ (1 + Real.log 16 + 6 / δ) * x ^ δ

Uniform from x=1, rather than an eventual bound with a varying cutoff.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_tau {δ : ℝ} (hδ : 0 < δ) : ∃ (Ca : ℝ), 0 < Ca ∧ ∀ (x : ℝ), 1 ≤ x → ∀ (a : ℤ), |↑a| ≤ x → ↑a.natAbs.divisors.card ≤ Ca * x ^ δ

A fixed tau constant precedes x and the signed shift.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_root_algebra {n r s V : ℝ} (hn : 0 < n) (hr : 0 < r) (hs : 0 < s) (_hV : 0 ≤ V) (κ : ℝ) : (16 * n * r * s * s) ^ (1 / 2 + κ) * (2 * r * √(8 * n * s * s * V)) = 8 * √8 * (16 * n * r * s * s) ^ κ * √V * n * r * √r * s ^ 2

Exact root algebra, retaining the Weil excess power as its own factor.