The moment recurrence when adjoining a new prime

The exact identity M_q(pn)=2 M_q(n)+E_q(n,p) is the starting point for the differential inequality in the weighted Hooley mean estimate.

theorem NairTenenbaum.hooleyWindow_prime_mul {p n : ℕ} (hp : Nat.Prime p) (hpn : ¬p ∣ n) (u : ℝ) : hooleyWindow (p * n) u = hooleyWindow n u + hooleyWindow n (u - Real.log ↑p)

noncomputable def NairTenenbaum.hooleyMixedMoment (j k n : ℕ) (a : ℝ) : ℝ

Mixed moments of a window and its translate.

Equations

• NairTenenbaum.hooleyMixedMoment j k n a = ∫ (u : ℝ), NairTenenbaum.hooleyWindow n u ^ j * NairTenenbaum.hooleyWindow n (u - a) ^ k

theorem NairTenenbaum.hooleyMixedMoment_nonneg (j k n : ℕ) (a : ℝ) : 0 ≤ hooleyMixedMoment j k n a

theorem NairTenenbaum.integrable_hooleyMixedMoment (j k n : ℕ) (a : ℝ) (hjk : 0 < j + k) : MeasureTheory.Integrable (fun (u : ℝ) => hooleyWindow n u ^ j * hooleyWindow n (u - a) ^ k) MeasureTheory.volume

@[simp]

theorem NairTenenbaum.hooleyMixedMoment_zero_left (q n : ℕ) (a : ℝ) : hooleyMixedMoment 0 q n a = hooleyMoment q n

@[simp]

theorem NairTenenbaum.hooleyMixedMoment_zero_right (q n : ℕ) (a : ℝ) : hooleyMixedMoment q 0 n a = hooleyMoment q n

theorem NairTenenbaum.hooleyMoment_prime_mul_expansion {p n q : ℕ} (hp : Nat.Prime p) (hpn : ¬p ∣ n) (hq : 0 < q) : hooleyMoment q (p * n) = ∑ j ∈ Finset.range (q + 1), hooleyMixedMoment j (q - j) n (Real.log ↑p) * ↑(q.choose j)

The complete binomial expansion, with integrability of every term proved.

noncomputable def NairTenenbaum.hooleyPrimeCrossMoment (q n p : ℕ) : ℝ

The positive mixed terms, with the two pure powers removed.

Equations

• NairTenenbaum.hooleyPrimeCrossMoment q n p = ∑ j ∈ Finset.Ico 1 q, NairTenenbaum.hooleyMixedMoment j (q - j) n (Real.log ↑p) * ↑(q.choose j)

theorem NairTenenbaum.hooleyPrimeCrossMoment_nonneg (q n p : ℕ) : 0 ≤ hooleyPrimeCrossMoment q n p

theorem NairTenenbaum.hooleyMoment_prime_mul {p n q : ℕ} (hp : Nat.Prime p) (hpn : ¬p ∣ n) (hq : 0 < q) : hooleyMoment q (p * n) = 2 * hooleyMoment q n + hooleyPrimeCrossMoment q n p

The recurrence used before equation (2.10) of the weighted mean proof.