Convergence of the auxiliary Euler products

The prime-power geometric estimates and the finite Euler product used in the preliminary lemmas of §4. No summability over all positive integers is assumed.

noncomputable def NairTenenbaum.auxiliaryRatio (ε : ℝ) (γ p : ℕ) : ℝ

The geometric ratio controlling the local series of f_h(n)/n.

Equations

• NairTenenbaum.auxiliaryRatio ε γ p = ↑p ^ (↑γ * ε - 1)

theorem NairTenenbaum.auxiliaryRatio_nonneg (ε : ℝ) (γ p : ℕ) : 0 ≤ auxiliaryRatio ε γ p

theorem NairTenenbaum.auxiliaryRatio_lt_one {ε : ℝ} {γ p : ℕ} (hp : Nat.Prime p) (hγε : ↑γ * ε < 1) : auxiliaryRatio ε γ p < 1

theorem NairTenenbaum.auxiliaryLocal_div_pow_le {A B ε : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : ℕ) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : auxiliaryLocal A B ε γ p ν / ↑p ^ ν ≤ B * auxiliaryRatio ε γ p ^ ν

theorem NairTenenbaum.auxiliaryLocal_summable {A B ε : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : ℕ) (hγε : ↑γ * ε < 1) {p : ℕ} (hp : Nat.Prime p) : Summable fun (ν : ℕ) => auxiliaryLocal A B ε γ p ν / ↑p ^ ν

theorem NairTenenbaum.auxiliaryLocal_tail_le {A B ε : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : ℕ) (hγε : ↑γ * ε < 1) {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : ∑' (ν : ℕ), auxiliaryLocal A B ε γ p (ν + N) / ↑p ^ (ν + N) ≤ B * auxiliaryRatio ε γ p ^ N / (1 - auxiliaryRatio ε γ p)

A uniform-in-exponent tail bound for a fixed prime.

theorem NairTenenbaum.auxiliary_smooth_hasSum {A B ε : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : ℕ) (hγε : ↑γ * ε < 1) (s : Finset ℕ) : HasSum (fun (n : ↑(Nat.factoredNumbers s)) => auxiliary A B ε γ ↑n / ↑↑n) (∏ p ∈ s with Nat.Prime p, ∑' (ν : ℕ), auxiliaryLocal A B ε γ p ν / ↑p ^ ν)

Finite Euler product over the integers whose prime factors belong to s.