The convolution kernel for exponential moments

The prime-power increments give exactly the local errors bounded in MomentPrimeBounds. Their multiplicative extension has a convergent Euler product on every finite prime support.

noncomputable def NairTenenbaum.momentIncrement (b : ℝ) (p ν : ℕ) : ℝ

The increment introduced by tilting a prime power by the moment exponent.

Equations

• NairTenenbaum.momentIncrement b p ν = (↑p ^ ν) ^ b - 1

theorem NairTenenbaum.momentIncrement_nonneg {b : ℝ} (hb : 0 ≤ b) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : 0 ≤ momentIncrement b p ν

theorem NairTenenbaum.primePowerProduct_one_add_momentIncrement (b : ℝ) (n : ℕ+) : primePowerProduct (fun (p ν : ℕ) => 1 + momentIncrement b p ν) ↑n = ↑↑n ^ b

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

Convolution kernel for the exponential moment comparison.

Equations

• NairTenenbaum.momentKernel A B ε β γ Q n = NairTenenbaum.rootAuxiliary A B ε γ Q n * NairTenenbaum.primePowerProduct (NairTenenbaum.momentIncrement (↑γ * β)) n

@[simp]

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

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

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

theorem NairTenenbaum.momentKernel_prime_pow_succ (A B ε β : ℝ) (γ : ℕ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : momentKernel A B ε β γ Q (p ^ (ν + 1)) = localMomentTerm A B ε β γ Q p ν

theorem NairTenenbaum.momentKernel_prime_pow_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 fun (ν : ℕ) => momentKernel A B ε β γ Q (p ^ ν)

theorem NairTenenbaum.momentKernel_local_tsum {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) : ∑' (ν : ℕ), momentKernel A B ε β γ Q (p ^ ν) = 1 + localMomentError A B ε β γ Q p

theorem NairTenenbaum.momentKernel_smooth_hasSum {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hβ : 0 ≤ β) (γ : ℕ) (hγ : ↑γ * (ε + β) < 1) (Q : Polynomial ℤ) (C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) (s : Finset ℕ) : HasSum (fun (n : ↑(Nat.factoredNumbers s)) => momentKernel A B ε β γ Q ↑n) (∏ p ∈ s with Nat.Prime p, (1 + localMomentError A B ε β γ Q p))

Exact Euler product for the moment convolution kernel.

theorem NairTenenbaum.momentKernel_sum_le_product {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hβ : 0 ≤ β) (γ : ℕ) (hγ : ↑γ * (ε + β) < 1) (Q : Polynomial ℤ) (C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) (s : Finset ℕ) (T : Finset ℕ+) (hT : ∀ n ∈ T, ↑n ∈ Nat.factoredNumbers s) : ∑ n ∈ T, momentKernel A B ε β γ Q ↑n ≤ ∏ p ∈ s with Nat.Prime p, (1 + localMomentError A B ε β γ Q p)

Every finite smooth partial sum is bounded by the kernel's Euler product.