Sampling Hooley windows at prime logarithms

The local integral comparison and the bounded prime mass on logarithmic intervals control the sampled moments, uniformly in the translation and the finite set of primes. This is the elementary input to the mixed-term bound in the weighted mean argument.

theorem NairTenenbaum.finite_sampling_le_integral {ι : Type u_1} (S : Finset ι) (w t : ι → ℝ) {f : ℝ → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hf₀ : ∀ (v : ℝ), 0 ≤ f v) {A C : ℝ} (hA : 0 ≤ A) (hw : ∀ i ∈ S, 0 ≤ w i) (hlocal : ∀ i ∈ S, f (t i) ≤ A * ∫ (v : ℝ) in Set.Ioc (t i - 1) (t i + 1), f v) (hoverlap : ∀ (v : ℝ), ∑ i ∈ S with v ∈ Set.Ioc (t i - 1) (t i + 1), w i ≤ C) : ∑ i ∈ S, w i * f (t i) ≤ A * C * ∫ (v : ℝ), f v

A finite collection of local integral majorants can be summed when their weighted overlap is bounded.

theorem NairTenenbaum.prime_log_overlap_bound (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (u v : ℝ) : ∑ p ∈ S with v ∈ Set.Ioc (u - Real.log ↑p - 1) (u - Real.log ↑p + 1), Real.log ↑p / ↑p ≤ Real.log 4 * Real.exp 2

theorem NairTenenbaum.prime_sampled_hooleyWindow_pow_le (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (n : ℕ) {q : ℕ} (hq : 0 < q) (u : ℝ) : ∑ p ∈ S, Real.log ↑p / ↑p * hooleyWindow n (u - Real.log ↑p) ^ q ≤ 2 ^ (q - 1) * (Real.log 4 * Real.exp 2) * hooleyMoment q n

Uniform prime sampling of every positive integral moment.