Root-weighted auxiliary Euler products

The local convergence needed in §4 now includes every prime, including primes dividing the discriminant. The bounds use the explicit uniform estimate for the root counts of each irreducible factor.

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

The multiplicative summand f_h(n) ρ_h(n) / n.

Equations

• NairTenenbaum.rootAuxiliary A B ε γ Q n = NairTenenbaum.auxiliary A B ε γ n * ↑(NairTenenbaum.rootCount Q n) / ↑n

@[simp]

theorem NairTenenbaum.rootAuxiliary_one (A B ε : ℝ) (γ : ℕ) (Q : Polynomial ℤ) : rootAuxiliary A B ε γ Q 1 = 1

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

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

theorem NairTenenbaum.Admissible.pullback_root_weight_le {k r : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (γ : Fin k → Fin r → ℕ) (Q : Fin r → Polynomial ℤ) (n : Tuple r) : pullback γ F n * ∏ h : Fin r, ↑(rootCount (Q h) ↑(n h)) / ↑↑(n h) ≤ F 1 * ∏ h : Fin r, rootAuxiliary A B ε (totalExponent γ h) (Q h) ↑(n h)

The pointwise majorization of the root-weighted summand used in §4.

theorem NairTenenbaum.rootAuxiliary_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) : rootAuxiliary A B ε γ Q (p ^ ν) ≤ ↑C * B * auxiliaryRatio ε γ p ^ ν

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

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

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