Bounded prime mass on logarithmic intervals

Chebyshev's elementary upper bound gives a uniform bound for Σ (log p)/p on every interval of logarithmic length two. This controls sampling the Hooley windows at prime logarithms.

theorem NairTenenbaum.prime_log_mass_exp_interval (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (L : ℝ) : ∑ p ∈ S with Real.exp L ≤ ↑p ∧ ↑p ≤ Real.exp (L + 2), Real.log ↑p / ↑p ≤ Real.log 4 * Real.exp 2

theorem NairTenenbaum.prime_log_mass_log_interval (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (L : ℝ) : ∑ p ∈ S with L ≤ Real.log ↑p ∧ Real.log ↑p ≤ L + 2, Real.log ↑p / ↑p ≤ Real.log 4 * Real.exp 2