Exponentially tilted auxiliary series

Multiplication by n^(γ β) is the exponential moment in the Rankin argument for Lemma 2. Its convergence is proved with the shifted exponent ε+β. The prime increment estimates retain the dependence on the cutoff explicitly.

noncomputable def NairTenenbaum.tiltedRootAuxiliary (A B ε β : ℝ) (γ : ℕ) (Q : Polynomial ℤ) (n : ℕ) : ℝ

The root auxiliary weight after exponential tilting.

Equations

• NairTenenbaum.tiltedRootAuxiliary A B ε β γ Q n = NairTenenbaum.rootAuxiliary A B ε γ Q n * ↑n ^ (↑γ * β)

@[simp]

theorem NairTenenbaum.tiltedRootAuxiliary_one (A B ε β : ℝ) (γ : ℕ) (Q : Polynomial ℤ) : tiltedRootAuxiliary A B ε β γ Q 1 = 1

theorem NairTenenbaum.tiltedRootAuxiliary_nonneg {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (γ : ℕ) (Q : Polynomial ℤ) (n : ℕ) : 0 ≤ tiltedRootAuxiliary A B ε β γ Q n

theorem NairTenenbaum.tiltedRootAuxiliary_mul (A B ε β : ℝ) (γ : ℕ) (Q : Polynomial ℤ) {m n : ℕ} (hmn : m.Coprime n) : tiltedRootAuxiliary A B ε β γ Q (m * n) = tiltedRootAuxiliary A B ε β γ Q m * tiltedRootAuxiliary A B ε β γ Q n

theorem NairTenenbaum.tiltedRootAuxiliary_prime_pow_le {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : ℕ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (C ν : ℕ) (hρ : rootCount Q (p ^ ν) ≤ C) : tiltedRootAuxiliary A B ε β γ Q (p ^ ν) ≤ ↑C * B * auxiliaryRatio (ε + β) γ p ^ ν

Tilting shifts the local geometric ratio from ε to ε+β.

theorem NairTenenbaum.tiltedRootAuxiliary_prime_pow_summable {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : ℕ) (hγ : ↑γ * (ε + β) < 1) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (C : ℕ) (hρ : ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : Summable fun (ν : ℕ) => tiltedRootAuxiliary A B ε β γ Q (p ^ ν)

noncomputable def NairTenenbaum.localMomentTerm (A B ε β : ℝ) (γ : ℕ) (Q : Polynomial ℤ) (p ν : ℕ) : ℝ

The local increment of the exponential moment, beginning at exponent one.

Equations

• NairTenenbaum.localMomentTerm A B ε β γ Q p ν = NairTenenbaum.rootAuxiliary A B ε γ Q (p ^ (ν + 1)) * ((↑p ^ (ν + 1)) ^ (↑γ * β) - 1)

noncomputable def NairTenenbaum.localMomentError (A B ε β : ℝ) (γ : ℕ) (Q : Polynomial ℤ) (p : ℕ) : ℝ

The local higher-order error in the tilted Euler factor.

Equations

• NairTenenbaum.localMomentError A B ε β γ Q p = ∑' (ν : ℕ), NairTenenbaum.localMomentTerm A B ε β γ Q p ν

theorem NairTenenbaum.localMomentTerm_nonneg {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hβ : 0 ≤ β) (γ : ℕ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : 0 ≤ localMomentTerm A B ε β γ Q p ν

theorem NairTenenbaum.localMomentTerm_le_tilted {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (γ : ℕ) (Q : Polynomial ℤ) (p ν : ℕ) : localMomentTerm A B ε β γ Q p ν ≤ tiltedRootAuxiliary A B ε β γ Q (p ^ (ν + 1))

theorem NairTenenbaum.localMomentTerm_summable {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hβ : 0 ≤ β) (γ : ℕ) (hγ : ↑γ * (ε + β) < 1) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (C : ℕ) (hρ : ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : Summable (localMomentTerm A B ε β γ Q p)

theorem NairTenenbaum.rootAuxiliary_prime_pow_le_A {A B ε : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : ℕ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (C ν : ℕ) (hρ : rootCount Q (p ^ ν) ≤ C) : rootAuxiliary A B ε γ Q (p ^ ν) ≤ ↑C * B * (A ^ γ / ↑p) ^ ν

The alternative geometric bound uses A^γ/p, which is sharper at large primes.

theorem NairTenenbaum.tiltedRootAuxiliary_prime_pow_le_A {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : ℕ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (C ν : ℕ) (hρ : rootCount Q (p ^ ν) ≤ C) : tiltedRootAuxiliary A B ε β γ Q (p ^ ν) ≤ ↑C * B * (A ^ γ * ↑p ^ (↑γ * β) / ↑p) ^ ν

A large-prime bound for the tilted series.

theorem NairTenenbaum.localMomentTerm_zero_le {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hβ : 0 ≤ β) (γ : ℕ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (C : ℕ) (hρ : rootCount Q p ≤ C) : localMomentTerm A B ε β γ Q p 0 ≤ ↑C * B * A ^ γ * ((↑p ^ (↑γ * β) - 1) / ↑p)

First-prime-power contribution to the moment error.

theorem NairTenenbaum.localMomentTerm_zero_sum_uniform {A B ε κ z : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (γ : ℕ) (Q : Polynomial ℤ) (C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → rootCount Q p ≤ C) : ∑ p ∈ Finset.Icc 0 ⌊z⌋₊ with Nat.Prime p, localMomentTerm A B ε (κ / Real.log z) γ Q p 0 ≤ ↑C * B * A ^ γ * (↑γ * κ * Real.exp (↑γ * κ) * Real.log 4 * (1 + (Real.log 2)⁻¹))

The first-power part of the exponential moment is uniform in z.