Reciprocal-density tails on fixed prime support

theorem NairTenenbaum.smooth_reciprocal_half_sum_le (s : Finset ℕ) (S : Finset ℕ+) (hS : ∀ n ∈ S, ↑n ∈ Nat.factoredNumbers s) : ∑ n ∈ S, ↑↑n ^ (-(1 / 2)) ≤ (1 / (1 - 2 ^ (-(1 / 2)))) ^ (Finset.filter Nat.Prime s).card

A geometric Euler-product bound for the reciprocal square roots of integers supported by finitely many primes.

theorem NairTenenbaum.smooth_root_density_tail_le (Q : Polynomial ℤ) (s : Finset ℕ) (M : ℕ) (hM : 1 ≤ M) (hρ : ∀ p ∈ s, Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ M) (S : Finset ℕ+) (hS : ∀ n ∈ S, ↑n ∈ Nat.factoredNumbers s) {T : ℝ} (hT : 0 < T) (hlarge : ∀ n ∈ S, T ≤ ↑↑n) : ∑ n ∈ S, ↑(rootCount Q ↑n) / ↑↑n ≤ ↑(M ^ (Finset.filter Nat.Prime s).card) * (1 / (1 - 2 ^ (-(1 / 2)))) ^ (Finset.filter Nat.Prime s).card * T ^ (-(1 / 2))

A large supported modulus supplies a square-root saving in its reciprocal root density. No pairwise coprimality assumption on the original divisors is needed.

theorem NairTenenbaum.PolynomialSystem.radical_rootCount_prime_pow_uniform {k r : ℕ} (P : PolynomialSystem k r) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : rootCount P.radical (p ^ ν) ≤ max P.total.natDegree (P.badDiscriminant ^ 3)

Uniform radical root counts at every prime power, including root-free primes and the restricted bad primes.