The totient correction in the sieve estimate

The correction for omitted sieve factors is (n/φ(n))^g. This module proves its multiplicativity, prime-power values, and the stronger weighted local convergence needed to replace the invalid general Lemma 1.

noncomputable def NairTenenbaum.totientTwist (g n : ℕ) : ℝ

The reciprocal-totient correction; the exponent is the polynomial degree.

Equations

• NairTenenbaum.totientTwist g n = (↑n / ↑n.totient) ^ g

@[simp]

theorem NairTenenbaum.totientTwist_one (g : ℕ) : totientTwist g 1 = 1

theorem NairTenenbaum.totientTwist_nonneg (g n : ℕ) : 0 ≤ totientTwist g n

theorem NairTenenbaum.totientTwist_mul (g : ℕ) {m n : ℕ} (hmn : m.Coprime n) : totientTwist g (m * n) = totientTwist g m * totientTwist g n

theorem NairTenenbaum.totientTwist_prime_pow (g : ℕ) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : totientTwist g (p ^ (ν + 1)) = (↑p / (↑p - 1)) ^ g

theorem NairTenenbaum.totientTwist_prime (g : ℕ) {p : ℕ} (hp : Nat.Prime p) : totientTwist g p = (↑p / (↑p - 1)) ^ g

theorem NairTenenbaum.totientTwist_prime_sub_one_le (g : ℕ) {p : ℕ} (hp : Nat.Prime p) : |totientTwist g p - 1| ≤ 2 * (2 ^ g - 1) / ↑p

An explicit O(1/p) bound with a constant depending only on the degree.