The sieve estimate after full bad-prime removal

The removed coordinates are replaced by a radical congruence at their least common multiple. Its full prime-power density is retained during summation.

def NairTenenbaum.badSieveModuli {r : ℕ} (u v : Tuple r) : Tuple (r + 1)

The pairwise coprime moduli used after grouping the bad-prime tuple by its least common multiple.

Equations

• NairTenenbaum.badSieveModuli u v = Fin.cons ⟨NairTenenbaum.tupleLCM u, ⋯⟩ v

@[simp]

theorem NairTenenbaum.badSieveModuli_zero {r : ℕ} (u v : Tuple r) : badSieveModuli u v 0 = ⟨tupleLCM u, ⋯⟩

@[simp]

theorem NairTenenbaum.badSieveModuli_succ {r : ℕ} (u v : Tuple r) (i : Fin r) : badSieveModuli u v i.succ = v i

theorem NairTenenbaum.mass_badSieveModuli {r : ℕ} (u v : Tuple r) : mass (badSieveModuli u v) = tupleLCM u * mass v

theorem NairTenenbaum.badSieveModuli_pairwise {r D : ℕ} (u v : Tuple r) (hv : Dagger D v) (hu : ∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers D.primeFactors) : Pairwise fun (i j : Fin (r + 1)) => (↑(badSieveModuli u v i)).Coprime ↑(badSieveModuli u v j)

theorem NairTenenbaum.totientTwist_badSieveModuli_le {r D : ℕ} (g : ℕ) (u v : Tuple r) (hD : D ≠ 0) (hu : ∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers D.primeFactors) : totientTwist g (mass (badSieveModuli u v)) ≤ totientTwist g D * ∏ i : Fin r, totientTwist g ↑(v i)

theorem NairTenenbaum.PolynomialSystem.congruenceSet_subset_badSieve {k r : ℕ} (P : PolynomialSystem k r) (u v : Tuple r) (a b : ℤ) : polynomialCongruenceSet P.R (u * v) a b ⊆ polynomialCongruenceSet (Fin.cons P.radical P.R) (badSieveModuli u v) a b

noncomputable def NairTenenbaum.PolynomialSystem.badPrimeSiftedCount {k r : ℕ} (P : PolynomialSystem k r) (u v : Tuple r) (a b : ℤ) (z : ℝ) : ℕ

The conditional sifted count for a bad part and a good divisor tuple.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.PolynomialSystem.badPrimeSiftedCount_le {k r : ℕ} (P : PolynomialSystem k r) (u v : Tuple r) (a b : ℤ) (z : ℝ) : P.badPrimeSiftedCount u v a b z ≤ conditionalPolynomialSiftedCount P.total (sieveModulus P.total (mass (badSieveModuli u v)) z) (Fin.cons P.radical P.R) (badSieveModuli u v) a b

theorem NairTenenbaum.PolynomialSystem.badSieveMainTerm_le {k r : ℕ} (P : PolynomialSystem k r) (g : ℕ) (u v : Tuple r) (hu : ∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors) (a b : ℤ) (hab : a ≤ b) (z : ℝ) : conditionalSieveMainTerm P.total g (Fin.cons P.radical P.R) (badSieveModuli u v) a b z ≤ ((↑b - ↑a) * sieveProduct P.total z * totientTwist g P.badDiscriminant * ∏ i : Fin r, totientTwist g ↑(v i)) * (↑(rootCount P.radical (tupleLCM u)) / ↑(tupleLCM u)) * ∏ i : Fin r, ↑(rootCount (P.R i) ↑(v i)) / ↑↑(v i)

theorem NairTenenbaum.exists_badPrime_sieve_bound {g : ℕ} (hg : 0 < g) {η δ : ℝ} (hη : 0 < η) (hδ : 0 < δ) : ∃ (K : ℝ) (L : ℝ), 1 ≤ K ∧ 1 ≤ L ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree ≤ g → ∀ (u v : Tuple r), Dagger P.badDiscriminant v → (∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors) → ∀ (a b : ℤ) (z : ℝ), a ≤ b → 2 ≤ z → 16 ≤ Real.log z → L * ↑(tupleLCM u) * ↑(mass v) * z ^ (4 * ↑g * (1 + η) + δ) ≤ ↑b - ↑a → ↑(P.badPrimeSiftedCount u v a b z) ≤ (K * (↑b - ↑a) * sieveProduct P.total z * totientTwist g P.badDiscriminant * ∏ i : Fin r, totientTwist g ↑(v i)) * (↑(rootCount P.radical (tupleLCM u)) / ↑(tupleLCM u)) * ∏ i : Fin r, ↑(rootCount (P.R i) ↑(v i)) / ↑↑(v i)

Pointwise sieve bound with all bad-prime valuations retained in the radical LCM density. The two constants depend only on the degree and chosen exponents.

noncomputable def NairTenenbaum.badPrimeSieveCost (B : ℝ) (g D : ℕ) : ℝ

The uniform cost of the full bad-prime sieve summation.

Equations

• NairTenenbaum.badPrimeSieveCost B g D = NairTenenbaum.totientTwist g D * NairTenenbaum.badPrimeMassBound B g D

theorem NairTenenbaum.PolynomialSystem.weighted_count_le_badPrimeKernel {k r : ℕ} (P : PolynomialSystem k r) {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (u v : Tuple r) (hcross : ∀ (i j : Fin r), (↑(u i)).Coprime ↑(v j)) {C count : ℝ} (hcount : 0 ≤ count) (hbound : count ≤ C * (↑(rootCount P.radical (tupleLCM u)) / ↑(tupleLCM u)) * ∏ i : Fin r, ↑(rootCount (P.R i) ↑(v i)) / ↑↑(v i)) : pullback P.exponent F (u * v) * count ≤ C * badPrimeTupleKernel A B ε (totalExponent P.exponent) P.radical u * rootTupleWeight P.exponent F P.R v

Transfer a count bound through the auxiliary weight of the bad-prime part. The coefficient includes any sieve correction specific to the argument set.

theorem NairTenenbaum.exists_badPrime_sieve_sum_bound {g : ℕ} (hg : 0 < g) {η δ : ℝ} (hη : 0 < η) (hδ : 0 < δ) : ∃ (K : ℝ) (L : ℝ), 1 ≤ K ∧ 1 ≤ L ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (A B ε : ℝ) (F : ArithmeticMap k), Admissible A B ε F → 0 ≤ A → 1 ≤ B → 0 < ε → ↑g ^ 2 * ε ≤ 1 / 8 → ∀ (S : Finset (Tuple r)) (v : Tuple r), Dagger P.badDiscriminant v → (∀ u ∈ S, ∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors) → ∀ (a b : ℤ) (z : ℝ), a ≤ b → 2 ≤ z → 16 ≤ Real.log z → (∀ u ∈ S, L * ↑(tupleLCM u) * ↑(mass v) * z ^ (4 * ↑g * (1 + η) + δ) ≤ ↑b - ↑a) → ∑ u ∈ S, pullback P.exponent F (u * v) * ↑(P.badPrimeSiftedCount u v a b z) ≤ K * badPrimeSieveCost B g P.badDiscriminant * (↑b - ↑a) * sieveProduct P.total z * rootTupleWeight P.exponent F P.R v * ∏ i : Fin r, totientTwist g ↑(v i)

Summing the entire bad-prime part costs only a degree/discriminant constant. The good tuple retains the totient-modified root weight required in the main proof.