Summable kernels for the corrected comparison

Multiplying the coprime majorant by the product of prime increments produces a convolution kernel. Its positive local terms are exactly the weighted tails proved convergent in ComparisonLocal.

noncomputable def NairTenenbaum.comparisonKernel (U l : ℕ → ℝ) (n : ℕ) : ℝ

The convolution kernel used in the arithmetic-weight comparison.

Equations

• NairTenenbaum.comparisonKernel U l n = U n * NairTenenbaum.radicalProduct l n

noncomputable def NairTenenbaum.kernelLocalError (U l : ℕ → ℝ) (p : ℕ) : ℝ

The higher-prime-power error of the comparison kernel.

Equations

• NairTenenbaum.kernelLocalError U l p = l p * ∑' (ν : ℕ), U (p ^ (ν + 1))

theorem NairTenenbaum.comparisonKernel_nonneg {U l : ℕ → ℝ} (hU : ∀ (n : ℕ), 0 ≤ U n) (hl : ∀ (p : ℕ), 0 ≤ l p) (n : ℕ) : 0 ≤ comparisonKernel U l n

theorem NairTenenbaum.kernelLocalError_nonneg {U l : ℕ → ℝ} (hU : ∀ (n : ℕ), 0 ≤ U n) (hl : ∀ (p : ℕ), 0 ≤ l p) (p : ℕ) : 0 ≤ kernelLocalError U l p

theorem NairTenenbaum.comparisonKernel_one {U l : ℕ → ℝ} (hU₁ : U 1 = 1) : comparisonKernel U l 1 = 1

theorem NairTenenbaum.comparisonKernel_mul {U l : ℕ → ℝ} (hU₀ : U 0 = 0) (hU : ∀ (m n : ℕ), m.Coprime n → U (m * n) = U m * U n) {m n : ℕ} (hmn : m.Coprime n) : comparisonKernel U l (m * n) = comparisonKernel U l m * comparisonKernel U l n

theorem NairTenenbaum.comparisonKernel_prime_pow_succ (U l : ℕ → ℝ) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : comparisonKernel U l (p ^ (ν + 1)) = l p * U (p ^ (ν + 1))

theorem NairTenenbaum.comparisonKernel_prime_pow_summable {U l : ℕ → ℝ} {p : ℕ} (hp : Nat.Prime p) (hs : Summable fun (ν : ℕ) => U (p ^ ν)) : Summable fun (ν : ℕ) => comparisonKernel U l (p ^ ν)

theorem NairTenenbaum.comparisonKernel_local_tsum {U l : ℕ → ℝ} (hU₁ : U 1 = 1) {p : ℕ} (hp : Nat.Prime p) (hs : Summable fun (ν : ℕ) => U (p ^ ν)) : ∑' (ν : ℕ), comparisonKernel U l (p ^ ν) = 1 + kernelLocalError U l p

theorem NairTenenbaum.comparisonKernel_smooth_hasSum {U l : ℕ → ℝ} (hU₀ : U 0 = 0) (hU₁ : U 1 = 1) (hU : ∀ (n : ℕ), 0 ≤ U n) (hl : ∀ (p : ℕ), 0 ≤ l p) (hmul : ∀ (m n : ℕ), m.Coprime n → U (m * n) = U m * U n) (hs : ∀ (p : ℕ), Nat.Prime p → Summable fun (ν : ℕ) => U (p ^ ν)) (s : Finset ℕ) : HasSum (fun (n : ↑(Nat.factoredNumbers s)) => comparisonKernel U l ↑n) (∏ p ∈ s with Nat.Prime p, (1 + kernelLocalError U l p))

Exact finite Euler product for the auxiliary convolution kernel.

theorem NairTenenbaum.comparisonKernel_sum_le_product {U l : ℕ → ℝ} (hU₀ : U 0 = 0) (hU₁ : U 1 = 1) (hU : ∀ (n : ℕ), 0 ≤ U n) (hl : ∀ (p : ℕ), 0 ≤ l p) (hmul : ∀ (m n : ℕ), m.Coprime n → U (m * n) = U m * U n) (hs : ∀ (p : ℕ), Nat.Prime p → Summable fun (ν : ℕ) => U (p ^ ν)) (N : ℕ+) : ∑ n ∈ Finset.Icc 1 N, comparisonKernel U l ↑n ≤ ∏ p ∈ Finset.range (↑N + 1) with Nat.Prime p, (1 + kernelLocalError U l p)

A kernel partial sum is bounded by its finite Euler product.

theorem NairTenenbaum.kernelLocalError_product_le {U l : ℕ → ℝ} (hU : ∀ (n : ℕ), 0 ≤ U n) (hl : ∀ (p : ℕ), 0 ≤ l p) (hs : Summable fun (p : Nat.Primes) => kernelLocalError U l ↑p) (s : Finset ℕ) : ∏ p ∈ s with Nat.Prime p, (1 + kernelLocalError U l p) ≤ Real.exp (∑' (p : Nat.Primes), kernelLocalError U l ↑p)

The finite Euler products have a uniform bound if their local errors are summable. The bound is independent of the cutoff.

theorem NairTenenbaum.unitary_comparison_uniform {w : ℕ+ → ℝ} {U l : ℕ → ℝ} (hw₀ : ∀ (n : ℕ+), 0 ≤ w n) (hU₀ : U 0 = 0) (hU₁ : U 1 = 1) (hU : ∀ (n : ℕ), 0 ≤ U n) (hl : ∀ (p : ℕ), 0 ≤ l p) (hmul : ∀ (m n : ℕ), m.Coprime n → U (m * n) = U m * U n) (hw : ∀ (a b : ℕ+), (↑a).Coprime ↑b → w (a * b) ≤ U ↑a * w b) (hs : ∀ (p : ℕ), Nat.Prime p → Summable fun (ν : ℕ) => U (p ^ ν)) (hE : Summable fun (p : Nat.Primes) => kernelLocalError U l ↑p) (N : ℕ+) : ∑ n ∈ Finset.Icc 1 N, w n * radicalProduct (fun (p : ℕ) => 1 + l p) ↑n ≤ Real.exp (∑' (p : Nat.Primes), kernelLocalError U l ↑p) * ∑ n ∈ Finset.Icc 1 N, w n

A corrected global comparison for scalar weights, with explicit sufficient hypotheses on their coprime majorant and prime increments.