Interpolation of Hooley's integral moments

Weighted arithmetic-geometric means give the interpolation between M₁=τ and M_q. This supplies the exponents of τ and M_q in the mixed-term estimate used in the weighted mean proof.

theorem NairTenenbaum.moment_interpolation_pointwise {x A B a b : ℝ} {j q : ℕ} (hx : 0 ≤ x) (hA : 0 < A) (hB : 0 < B) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hexp : a + ↑q * b = ↑j) (hj : 0 < j) : x ^ j ≤ A ^ a * B ^ b * (a * (x / A) + b * (x ^ q / B))

theorem NairTenenbaum.hooleyMoment_interpolation (n : ℕ) {j q : ℕ} (hq : 1 < q) (hj : 1 ≤ j) (hjq : j ≤ q) : hooleyMoment j n ≤ ↑n.divisors.card ^ ((↑q - ↑j) / (↑q - 1)) * hooleyMoment q n ^ ((↑j - 1) / (↑q - 1))

theorem NairTenenbaum.hooleyMoment_mixedProduct_le (n : ℕ) {j q : ℕ} (hq : 1 < q) (hj : 1 ≤ j) (hjq : j < q) : hooleyMoment j n * hooleyMoment (q - j) n ≤ ↑n.divisors.card ^ (↑q / (↑q - 1)) * hooleyMoment q n ^ ((↑q - 2) / (↑q - 1))

The product of the complementary moments has exponents independent of the binomial index.