Full bad-prime summation for the prime-argument sieve

The original radical and restricted discriminant control the bad-prime coordinates. Adjoining the argument only adds a totient power and the explicit constant-term/logarithm factor.

noncomputable def NairTenenbaum.primeArgumentFactor (Q : Polynomial ℤ) (z : ℝ) : ℝ

The constant-term totient correction divided by the logarithmic sieve cutoff.

Equations

• NairTenenbaum.primeArgumentFactor Q z = NairTenenbaum.totientTwist 1 (Polynomial.eval 0 Q).natAbs / Real.log z

theorem NairTenenbaum.primeArgumentFactor_nonneg (Q : Polynomial ℤ) {z : ℝ} (hz : 1 ≤ z) : 0 ≤ primeArgumentFactor Q z

theorem NairTenenbaum.primeArgumentConditionalMainTerm_eq {r : ℕ} (Q : Polynomial ℤ) (g : ℕ) (R : Fin r → Polynomial ℤ) (m : Tuple r) (a b : ℤ) (z : ℝ) : primeArgumentConditionalMainTerm Q g R m a b z = conditionalSieveMainTerm Q (g + 1) R m a b z * primeArgumentFactor Q z

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

The conditional prime-argument count after splitting off all bad-prime powers.

Equations

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

theorem NairTenenbaum.PolynomialSystem.primeArgumentBadSiftedCount_le {k r : ℕ} (P : PolynomialSystem k r) (g : ℕ) (u v : Tuple r) (a b : ℤ) (z : ℝ) : P.primeArgumentBadSiftedCount g u v a b z ≤ conditionalPolynomialSiftedCount (P.total * Polynomial.X) (primeArgumentSieveModulus P.total g (mass (badSieveModuli u v)) z) (Fin.cons P.radical P.R) (badSieveModuli u v) a b

theorem NairTenenbaum.exists_primeArgument_bad_sieve_bound (g : ℕ) {η δ : ℝ} (hη : 0 < η) (hδ : 0 < δ) : ∃ (K : ℝ) (L : ℝ), 1 ≤ K ∧ 1 ≤ L ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree ≤ g → Polynomial.eval 0 P.total ≠ 0 → ∀ (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) * (1 + η) + δ) ≤ ↑b - ↑a → ↑(P.primeArgumentBadSiftedCount g u v a b z) ≤ ((K * (↑b - ↑a) * sieveProduct P.total z * totientTwist (g + 1) P.badDiscriminant * ∏ i : Fin r, totientTwist (g + 1) ↑(v i)) * (↑(rootCount P.radical (tupleLCM u)) / ↑(tupleLCM u)) * ∏ i : Fin r, ↑(rootCount (P.R i) ↑(v i)) / ↑↑(v i)) * primeArgumentFactor P.total z

All bad-prime valuations stay in the original radical LCM density.

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

The uniform cost of summing bad-prime parts in the prime-argument sieve.

Equations

• NairTenenbaum.primeArgumentBadSieveCost B g D = NairTenenbaum.totientTwist (g + 1) D * NairTenenbaum.badPrimeMassBound B g D

theorem NairTenenbaum.exists_primeArgument_bad_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 → Polynomial.eval 0 P.total ≠ 0 → ∀ (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) * (1 + η) + δ) ≤ ↑b - ↑a) → ∑ u ∈ S, pullback P.exponent F (u * v) * ↑(P.primeArgumentBadSiftedCount g u v a b z) ≤ (K * primeArgumentBadSieveCost B g P.badDiscriminant * (↑b - ↑a) * sieveProduct P.total z * rootTupleWeight P.exponent F P.R v * ∏ i : Fin r, totientTwist (g + 1) ↑(v i)) * primeArgumentFactor P.total z