Fractional powers in the weighted prime step

Concavity supplies the finite weighted Hölder bound required when the Dirichlet series uses M_q(n)^(t/q) with 0<t≤q.

theorem NairTenenbaum.weighted_sum_rpow_le {ι : Type u_1} (S : Finset ι) (w f : ι → ℝ) (hw : ∀ i ∈ S, 0 ≤ w i) (hf : ∀ i ∈ S, 0 ≤ f i) {θ : ℝ} (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) : ∑ i ∈ S, w i * f i ^ θ ≤ (∑ i ∈ S, w i) ^ (1 - θ) * (∑ i ∈ S, w i * f i) ^ θ

noncomputable def NairTenenbaum.hooleyPrimeErrorBound (Q : Polynomial ℤ) (q n : ℕ) : ℝ

The explicit mixed error in the weighted prime recurrence.

Equations

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

theorem NairTenenbaum.hooleyPrimeErrorBound_nonneg (Q : Polynomial ℤ) (q n : ℕ) : 0 ≤ hooleyPrimeErrorBound Q q n

theorem NairTenenbaum.root_weighted_hooleyMoment_rpow_prime_step {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (n : ℕ) {q : ℕ} (hq : 1 < q) {σ θ : ℝ} (hσ : 1 ≤ σ) (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) : ∑ p ∈ S with ¬p ∣ n, rootPrimeLogWeight Q σ p * hooleyMoment q (p * n) ^ θ ≤ (2 * hooleyMoment q n) ^ θ * ∑ p ∈ S, rootPrimeLogWeight Q σ p + (∑ p ∈ S, rootPrimeLogWeight Q σ p) ^ (1 - θ) * hooleyPrimeErrorBound Q q n ^ θ

The finite prime bound for the fractional moment used in the Dirichlet series. Its main prime sum is left explicit for the prime-ideal input.