Prime expansion of the Dirichlet-series derivative

The reindexing in (2.9) of the weighted Hooley mean proof retains squarefree support and the exclusion of primes dividing the cofactor. Its convergence follows from the already proved logarithmic Dirichlet-series convergence.

noncomputable def NairTenenbaum.hooleyPrimeDirichletTerm (Q : Polynomial ℤ) (t : ℝ) (q : ℕ) (σ : ℝ) (p m : ℕ) : ℝ

The prime-step term in the Dirichlet expansion of the Hooley moment.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.hooleyPrimeDirichletTerm_nonneg (Q : Polynomial ℤ) (t : ℝ) (q : ℕ) (σ : ℝ) {p : ℕ} (hp : Nat.Prime p) (m : ℕ) : 0 ≤ hooleyPrimeDirichletTerm Q t q σ p m

@[simp]

theorem NairTenenbaum.hooleyPrimeDirichletTerm_zero (Q : Polynomial ℤ) (t : ℝ) (q : ℕ) (σ : ℝ) (p : ℕ) : hooleyPrimeDirichletTerm Q t q σ p 0 = 0

theorem NairTenenbaum.hooleyPrimeDirichletTerm_eq (Q : Polynomial ℤ) (t : ℝ) (q : ℕ) (σ : ℝ) {p : ℕ} (hp : Nat.Prime p) (m : ℕ) : hooleyMomentCoefficient Q t q (p * m) * ↑(p * m) ^ (-σ) * Real.log ↑p = hooleyPrimeDirichletTerm Q t q σ p m

theorem NairTenenbaum.summable_hooleyPrimeDirichletTerm {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hσ : 1 < σ) : Summable fun (x : Nat.Primes × ℕ+) => hooleyPrimeDirichletTerm Q t q σ ↑x.1 ↑x.2

theorem NairTenenbaum.neg_deriv_hooleyDirichlet_eq_prime_sum {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hσ : 1 < σ) : -deriv (hooleyDirichlet Q t q) σ = ∑' (p : Nat.Primes) (m : ℕ), hooleyPrimeDirichletTerm Q t q σ (↑p) m

theorem NairTenenbaum.summable_hooleyPrimeDirichletTerm_nat {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hσ : 1 < σ) : Summable fun (x : Nat.Primes × ℕ) => hooleyPrimeDirichletTerm Q t q σ (↑x.1) x.2

theorem NairTenenbaum.neg_deriv_hooleyDirichlet_eq_cofactor_sum {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hσ : 1 < σ) : -deriv (hooleyDirichlet Q t q) σ = ∑' (n : ℕ) (p : Nat.Primes), hooleyPrimeDirichletTerm Q t q σ (↑p) n