Summing the small-divisor sieve estimate

The full bad-prime summation and corrected multivariable totient comparison combine into a bound by the original truncated weight, with uniform constants.

theorem NairTenenbaum.PolynomialSystem.dagger_bad_of_dagger {k r : ℕ} (P : PolynomialSystem k r) {v : Tuple r} (hv : Dagger P.discriminant v) : Dagger P.badDiscriminant v

theorem NairTenenbaum.positiveUpTo_pnat (N : ℕ+) : positiveUpTo ↑↑N = Finset.Icc 1 N

theorem NairTenenbaum.PolynomialSystem.totient_tuple_sum_le {k r : ℕ} (P : PolynomialSystem k r) {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hgε : ↑P.total.natDegree * ε < 1) (N : ℕ+) : ∑ v ∈ weightUpTo P.exponent P.discriminant N, rootTupleWeight P.exponent F P.R v * ∏ i : Fin r, totientTwist P.total.natDegree ↑(v i) ≤ totientComparisonBound B ε P.total.natDegree P.badDiscriminant * ∑ n ∈ Finset.Icc 1 N, P.weight F n

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

The product of the bad-prime sieve and totient-comparison costs.

Equations

• NairTenenbaum.smallDivisorSieveCost B ε g D = NairTenenbaum.badPrimeSieveCost B g D * NairTenenbaum.totientComparisonBound B ε g D

theorem NairTenenbaum.exists_smallDivisor_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 → ∀ (N : ℕ+) (S : Tuple r → Finset (Tuple r)), (∀ v ∈ weightUpTo P.exponent P.discriminant N, ∀ u ∈ S v, ∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors) → ∀ (a b : ℤ) (z : ℝ), a ≤ b → 2 ≤ z → 16 ≤ Real.log z → (∀ v ∈ weightUpTo P.exponent P.discriminant N, ∀ u ∈ S v, L * ↑(tupleLCM u) * ↑(mass v) * z ^ (4 * ↑g * (1 + η) + δ) ≤ ↑b - ↑a) → ∑ v ∈ weightUpTo P.exponent P.discriminant N, ∑ u ∈ S v, pullback P.exponent F (u * v) * ↑(P.badPrimeSiftedCount u v a b z) ≤ K * smallDivisorSieveCost B ε g P.badDiscriminant * (↑b - ↑a) * sieveProduct P.total z * ∑ n ∈ Finset.Icc 1 N, P.weight F n

A finite family of bad-prime parts over all small dagger tuples is bounded by the original weight sum. The sieve level is required only for the parts actually present in each finite family.