Prime averages of the mixed terms

Prime sampling and interpolation prove the mixed-term estimate needed before equation (2.10) of Tenenbaum's weighted mean argument. The estimate holds for every finite set of primes, with constants independent of that set.

theorem NairTenenbaum.prime_sum_hooleyMixedMoment_le (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (n : ℕ) {j k : ℕ} (hj : 0 < j) (hk : 0 < k) : ∑ p ∈ S, Real.log ↑p / ↑p * hooleyMixedMoment j k n (Real.log ↑p) ≤ 2 ^ (k - 1) * (Real.log 4 * Real.exp 2) * (hooleyMoment j n * hooleyMoment k n)

theorem NairTenenbaum.prime_sum_hooleyMixedMoment_interpolated (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (n : ℕ) {j q : ℕ} (hq : 1 < q) (hj : 1 ≤ j) (hjq : j < q) : ∑ p ∈ S, Real.log ↑p / ↑p * hooleyMixedMoment j (q - j) n (Real.log ↑p) ≤ 2 ^ q * (Real.log 4 * Real.exp 2) * (↑n.divisors.card ^ (↑q / (↑q - 1)) * hooleyMoment q n ^ ((↑q - 2) / (↑q - 1)))

The complementary moment factors no longer depend on the binomial index.

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

The finite prime mixed-term estimate, with the same 4^q order and moment exponents as the weighted mean proof.