A sufficient weighted local hypothesis for the comparison argument

The printed Lemma 1 is false for general multiplicative twists. This module checks the local convergence step for twists constant on positive powers of each prime and satisfying |θ(p)-1| ≤ L/p. These hypotheses cover the shape of the totient correction used in the main proof, once its elementary estimates are supplied. The global finite-weight comparison is still a separate step.

theorem NairTenenbaum.rootAuxiliary_tail_le {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) (N : ℕ) : ∑' (ν : ℕ), rootAuxiliary A B ε γ Q (p ^ (ν + N)) ≤ ↑C * B * auxiliaryRatio ε γ p ^ N / (1 - auxiliaryRatio ε γ p)

The geometric estimate remains valid for every root-weighted local tail.

noncomputable def NairTenenbaum.localComparisonError (A B ε : ℝ) (γ : ℕ) (Q : Polynomial ℤ) (θ : ℕ → ℝ) (p : ℕ) : ℝ

The local expression which actually occurs after splitting the divisor convolution in the proof of Lemma 1.

Equations

• NairTenenbaum.localComparisonError A B ε γ Q θ p = ∑' (ν : ℕ), |θ (p ^ (ν + 1)) - θ (p ^ ν)| * ∑' (j : ℕ), NairTenenbaum.rootAuxiliary A B ε γ Q (p ^ (j + (ν + 1)))

theorem NairTenenbaum.localComparisonError_nonneg {A B ε : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (γ : ℕ) (Q : Polynomial ℤ) (θ : ℕ → ℝ) (p : ℕ) : 0 ≤ localComparisonError A B ε γ Q θ p

theorem NairTenenbaum.localComparisonError_eq (A B ε : ℝ) (γ : ℕ) (Q : Polynomial ℤ) {θ : ℕ → ℝ} (hθ₁ : θ 1 = 1) {p : ℕ} (hθ : ∀ (ν : ℕ), θ (p ^ (ν + 1)) = θ p) : localComparisonError A B ε γ Q θ p = |θ p - 1| * ∑' (j : ℕ), rootAuxiliary A B ε γ Q (p ^ (j + 1))

For a twist constant on positive prime powers, only the first difference contributes to the corrected weighted hypothesis.

theorem NairTenenbaum.localComparisonError_le {A B ε L : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hL : 0 ≤ L) (γ : ℕ) (hγε : ↑γ * ε < 1) (Q : Polynomial ℤ) {θ : ℕ → ℝ} (hθ₁ : θ 1 = 1) {p : ℕ} (hp : Nat.Prime p) (hθ : ∀ (ν : ℕ), θ (p ^ (ν + 1)) = θ p) (hθp : |θ p - 1| ≤ L / ↑p) (C : ℕ) (hρ : ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : localComparisonError A B ε γ Q θ p ≤ L * ↑C * B / (1 - auxiliaryRatio ε γ 2) * ↑p ^ (↑γ * ε - 2)

A pointwise summable bound for the corrected local expression.

theorem NairTenenbaum.localComparisonError_summable {A B ε L : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hL : 0 ≤ L) (γ : ℕ) (hγε : ↑γ * ε < 1) (Q : Polynomial ℤ) {θ : ℕ → ℝ} (hθ₁ : θ 1 = 1) (hθ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), θ (p ^ (ν + 1)) = θ p) (hθp : ∀ (p : ℕ), Nat.Prime p → |θ p - 1| ≤ L / ↑p) (C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : Summable fun (p : Nat.Primes) => localComparisonError A B ε γ Q θ ↑p

The weighted local errors are summable over all primes under the explicit stronger hypotheses; no use is made of the invalid printed Lemma 1.

theorem NairTenenbaum.localComparisonError_tsum_le {A B ε L : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hL : 0 ≤ L) (γ : ℕ) (hγε : ↑γ * ε < 1) (Q : Polynomial ℤ) {θ : ℕ → ℝ} (hθ₁ : θ 1 = 1) (hθ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), θ (p ^ (ν + 1)) = θ p) (hθp : ∀ (p : ℕ), Nat.Prime p → |θ p - 1| ≤ L / ↑p) (C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : ∑' (p : Nat.Primes), localComparisonError A B ε γ Q θ ↑p ≤ L * ↑C * B / (1 - auxiliaryRatio ε γ 2) * ∑' (n : ℕ), ↑n ^ (↑γ * ε - 2)

A total bound depending only on the growth parameters and the root/twist bounds, rather than on the coefficients of the individual polynomial.