Euler factors omitted at primes dividing the conditioning modulus

The omitted factors are bounded by a uniform constant times (n/φ(n))^g. The quotient of the local factors differs from one by O(g²/p²) outside the finitely many primes at most 2g.

theorem NairTenenbaum.one_sub_pow_le_quadratic (g : ℕ) {t : ℝ} (ht : 0 ≤ t) (ht₁ : t ≤ 1) : (1 - t) ^ g ≤ 1 - ↑g * t + ↑g ^ 2 * t ^ 2

noncomputable def NairTenenbaum.omittedEulerRatio (Q : Polynomial ℤ) (g p : ℕ) : ℝ

The correction ratio for the Euler factors omitted from the sieve.

Equations

• NairTenenbaum.omittedEulerRatio Q g p = (1 - 1 / ↑p) ^ g / (1 - ↑(NairTenenbaum.rootCount Q p) / ↑p)

theorem NairTenenbaum.omittedEulerRatio_nonneg {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (g : ℕ) {p : ℕ} (hp : Nat.Prime p) : 0 ≤ omittedEulerRatio Q g p

theorem NairTenenbaum.omittedEulerRatio_le_prime {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (g : ℕ) {p : ℕ} (hp : Nat.Prime p) : omittedEulerRatio Q g p ≤ ↑p

theorem NairTenenbaum.omittedEulerRatio_le_exp {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {g p : ℕ} (hg : Q.natDegree ≤ g) (hp : Nat.Prime p) (hlarge : 2 * g ≤ p) : omittedEulerRatio Q g p ≤ Real.exp (2 * ↑g ^ 2 / ↑p ^ 2)

noncomputable def NairTenenbaum.omittedEulerBound (g : ℕ) : ℝ

A uniform upper bound for the omitted Euler-factor ratio.

Equations

• NairTenenbaum.omittedEulerBound g = (2 * ↑g + 1) ^ (2 * g + 1) * Real.exp (2 * ↑g ^ 2 * ∑' (n : ℕ), 1 / ↑n ^ 2)

theorem NairTenenbaum.omittedEulerBound_pos (g : ℕ) : 0 < omittedEulerBound g

theorem NairTenenbaum.omittedEulerRatio_prod_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {g : ℕ} (hg : Q.natDegree ≤ g) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : ∏ p ∈ S, omittedEulerRatio Q g p ≤ omittedEulerBound g

theorem NairTenenbaum.totientTwist_one_le (g : ℕ) {n : ℕ} (hn : n ≠ 0) : 1 ≤ totientTwist g n

theorem NairTenenbaum.totientTwist_eq_prod (g : ℕ) {n : ℕ} (hn : n ≠ 0) : totientTwist g n = ∏ p ∈ n.primeFactors, totientTwist g p

theorem NairTenenbaum.omittedEulerRatio_mul_totient (Q : Polynomial ℤ) (g : ℕ) {p : ℕ} (hp : Nat.Prime p) : omittedEulerRatio Q g p * totientTwist g p = (1 - ↑(rootCount Q p) / ↑p)⁻¹

theorem NairTenenbaum.omittedEulerFactors_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {g n : ℕ} (hg : Q.natDegree ≤ g) (hn : n ≠ 0) (S : Finset ℕ) (hS : S ⊆ n.primeFactors) : ∏ p ∈ S, (1 - ↑(rootCount Q p) / ↑p)⁻¹ ≤ omittedEulerBound g * totientTwist g n

The missing Euler factors over any subset of the modulus prime factors are controlled by the standard totient correction and a degree-only constant.