Euler products on a band of primes

A logarithmic prime estimate bounds the first powers on w < p ≤ z. When γ ε < 1/2, all higher powers have a convergent power-series majorant, uniform in both endpoints. This gives the prime-band constant needed for the last truncation step in Lemma 2.

noncomputable def NairTenenbaum.primeBandNumbers (w z : ℝ) : Finset ℕ

Integers supported on the primes in a specified band.

Equations

• NairTenenbaum.primeBandNumbers w z = {p ∈ Finset.Icc 0 ⌊z⌋₊ | w < ↑p}

theorem NairTenenbaum.primeBand_reciprocal_sum_le {w z : ℝ} (hw : 2 ≤ w) (hz : 2 ≤ z) : ∑ p ∈ primeBandNumbers w z with Nat.Prime p, (↑p)⁻¹ ≤ Real.log 4 * (1 + Real.log z) / Real.log w

An elementary bound for the reciprocal prime sum on a band.

theorem NairTenenbaum.rootAuxiliary_geometric_tail_le {A B ε M q : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (γ : ℕ) (Q : Polynomial ℤ) (p : ℕ) (hq₀ : 0 ≤ q) (hq₁ : q < 1) (hbound : ∀ (ν : ℕ), rootAuxiliary A B ε γ Q (p ^ ν) ≤ M * q ^ ν) (N : ℕ) : ∑' (ν : ℕ), rootAuxiliary A B ε γ Q (p ^ (ν + N)) ≤ M * q ^ N / (1 - q)

Tail of the un-tilted local root auxiliary under a geometric majorant.

theorem NairTenenbaum.rootAuxiliary_higher_le {A B ε σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 1) (γ : ℕ) (hγ : ↑γ * ε ≤ σ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (C : ℕ) (hρ : ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : ∑' (ν : ℕ), rootAuxiliary A B ε γ Q (p ^ (ν + 2)) ≤ ↑C * B / (1 - 2 ^ (σ - 1)) * ↑p ^ (2 * σ - 2)

A summable power bound for all powers of a prime starting at the square.

noncomputable def NairTenenbaum.rootHigherMajorant (B σ : ℝ) (C n : ℕ) : ℝ

A summable majorant for higher prime-power root contributions.

Equations

• NairTenenbaum.rootHigherMajorant B σ C n = ↑C * B / (1 - 2 ^ (σ - 1)) * ↑n ^ (2 * σ - 2)

theorem NairTenenbaum.rootHigherMajorant_nonneg {B σ : ℝ} (hB : 0 ≤ B) (hσ : σ < 1) (C n : ℕ) : 0 ≤ rootHigherMajorant B σ C n

theorem NairTenenbaum.rootHigherMajorant_summable (B : ℝ) {σ : ℝ} (hσ : σ < 1 / 2) (C : ℕ) : Summable (rootHigherMajorant B σ C)

theorem NairTenenbaum.rootAuxiliary_higher_sum_le {A B ε σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 1 / 2) (γ : ℕ) (hγ : ↑γ * ε ≤ σ) (Q : Polynomial ℤ) (C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) (s : Finset ℕ) : ∑ p ∈ s with Nat.Prime p, ∑' (ν : ℕ), rootAuxiliary A B ε γ Q (p ^ (ν + 2)) ≤ ∑' (n : ℕ), rootHigherMajorant B σ C n

The higher prime powers have a bound independent of the prime set.

noncomputable def NairTenenbaum.primeBandBound (A B σ L : ℝ) (γ C : ℕ) : ℝ

The prime-band Euler-product bound depends only on the logarithm ratio.

Equations

• NairTenenbaum.primeBandBound A B σ L γ C = Real.exp (↑C * B * A ^ γ * Real.log 4 * (L + (Real.log 2)⁻¹) + ∑' (n : ℕ), NairTenenbaum.rootHigherMajorant B σ C n)

theorem NairTenenbaum.rootAuxiliary_primeBand_product_le {A B ε σ L w z : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 1 / 2) (hw : 2 ≤ w) (hz : 2 ≤ z) (hlog : Real.log z / Real.log w ≤ L) (γ : ℕ) (hγ : ↑γ * ε ≤ σ) (Q : Polynomial ℤ) (C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : ∏ p ∈ primeBandNumbers w z with Nat.Prime p, ∑' (ν : ℕ), rootAuxiliary A B ε γ Q (p ^ ν) ≤ primeBandBound A B σ L γ C