Integral moments of Hooley's divisor windows

These moments are the analytic starting point of the weighted mean estimate in Tenenbaum, Sur une question d'Erdős et Schinzel, II, Lemma 2.2. Integrability is proved from the finite indicator representation, including the convention at n=0.

noncomputable def NairTenenbaum.hooleyWindow (n : ℕ) (u : ℝ) : ℝ

The divisor count in a logarithmic window used to define Hooley's function.

Equations

• NairTenenbaum.hooleyWindow n u = ↑(NairTenenbaum.divisorWindow n u)

theorem NairTenenbaum.hooleyWindow_nonneg (n : ℕ) (u : ℝ) : 0 ≤ hooleyWindow n u

theorem NairTenenbaum.hooleyWindow_le_card (n : ℕ) (u : ℝ) : hooleyWindow n u ≤ ↑n.divisors.card

theorem NairTenenbaum.hooleyWindow_eq_sum_indicator (n : ℕ) (u : ℝ) : hooleyWindow n u = ∑ d ∈ n.divisors, (Set.Ico (Real.log ↑d - 1) (Real.log ↑d)).indicator (fun (x : ℝ) => 1) u

theorem NairTenenbaum.measurable_hooleyWindow (n : ℕ) : Measurable (hooleyWindow n)

theorem NairTenenbaum.integrable_hooleyWindow (n : ℕ) : MeasureTheory.Integrable (hooleyWindow n) MeasureTheory.volume

theorem NairTenenbaum.integral_hooleyWindow (n : ℕ) : ∫ (u : ℝ), hooleyWindow n u = ↑n.divisors.card

theorem NairTenenbaum.integrable_hooleyWindow_pow (n : ℕ) {q : ℕ} (hq : 0 < q) : MeasureTheory.Integrable (fun (u : ℝ) => hooleyWindow n u ^ q) MeasureTheory.volume

noncomputable def NairTenenbaum.hooleyMoment (q n : ℕ) : ℝ

The moment M_q(n); positive orders are the integrable ones used below.

Equations

• NairTenenbaum.hooleyMoment q n = ∫ (u : ℝ), NairTenenbaum.hooleyWindow n u ^ q

theorem NairTenenbaum.hooleyMoment_nonneg (q n : ℕ) : 0 ≤ hooleyMoment q n

@[simp]

theorem NairTenenbaum.hooleyMoment_one (n : ℕ) : hooleyMoment 1 n = ↑n.divisors.card

@[simp]

theorem NairTenenbaum.hooleyMoment_at_zero {q : ℕ} (hq : 0 < q) : hooleyMoment q 0 = 0

theorem NairTenenbaum.hooleyMoment_le_card_pow (n : ℕ) {q : ℕ} (hq : 0 < q) : hooleyMoment q n ≤ ↑n.divisors.card ^ q

The elementary upper half of the moment comparison (2.6).