From Dirichlet moments to finite squarefree Hooley sums

A Rankin comparison at σ=1+1/log x costs only exp(1). The comparison between the maximum window and an integral moment costs at most 2^t.

theorem NairTenenbaum.hooleyDelta_rpow_le_moment_rpow (n : ℕ) {q : ℕ} (hq : 0 < q) {t : ℝ} (ht : 0 ≤ t) : ↑(hooleyDelta n) ^ t ≤ 2 ^ t * hooleyMoment q n ^ (t / ↑q)

theorem NairTenenbaum.reciprocal_le_rankin_weight {x σ : ℝ} (hσ : 1 ≤ σ) {n : ℕ} (hn : 0 < n) (hnx : ↑n ≤ x) : (↑n)⁻¹ ≤ x ^ (σ - 1) * ↑n ^ (-σ)

theorem NairTenenbaum.finite_reciprocal_hooleyMoment_le_dirichlet {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t x σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hx : 0 < x) (hσ : 1 < σ) (S : Finset ℕ) (hS : ∀ n ∈ S, 0 < n ∧ ↑n ≤ x) : ∑ n ∈ S, hooleyMomentCoefficient Q t q n / ↑n ≤ x ^ (σ - 1) * hooleyDirichlet Q t q σ

noncomputable def NairTenenbaum.squarefreeHooleyRootSum (Q : Polynomial ℤ) (t x : ℝ) : ℝ

The Hooley root sum restricted to squarefree integers.

Equations

• NairTenenbaum.squarefreeHooleyRootSum Q t x = ∑ n ∈ Finset.Icc 1 ⌊x⌋₊ with Squarefree n, ↑(NairTenenbaum.hooleyDelta n) ^ t * ↑(NairTenenbaum.rootCount Q n) / ↑n

theorem NairTenenbaum.squarefreeHooleyRootSum_le_dirichlet {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t x σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hx : 0 < x) (hσ : 1 < σ) : squarefreeHooleyRootSum Q t x ≤ 2 ^ t * x ^ (σ - 1) * hooleyDirichlet Q t q σ

theorem NairTenenbaum.squarefreeHooleyRootSum_le_log_dirichlet {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t x : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hx : 1 < x) : squarefreeHooleyRootSum Q t x ≤ 2 ^ t * Real.exp 1 * hooleyDirichlet Q t q (1 + 1 / Real.log x)