The factored weight bound for pairwise coprime polynomials

Tuples are first grouped by their original substituted arguments. The combined density of each fiber is bounded by the corresponding product of original-polynomial root densities. Only then is the mass cutoff enlarged to a box and the independent one-variable sums multiplied.

noncomputable def NairTenenbaum.rootWeightedSum (Q : Polynomial ℤ) (F : ArithmeticMap 1) (x : ℝ) : ℝ

The one-variable root-weighted sum appearing in Corollary 3.

Equations

• NairTenenbaum.rootWeightedSum Q F x = ∑ n ∈ NairTenenbaum.positiveUpTo x, (F fun (x : Fin 1) => n) * (↑(NairTenenbaum.rootCount Q ↑n) / ↑↑n)

theorem NairTenenbaum.PolynomialSystem.sum_weight_product_le {k r : ℕ} (P : PolynomialSystem k r) (hcop : ∀ (i j : Fin k), i ≠ j → IsCoprime (Polynomial.map (Int.castRingHom ℚ) (P.Q i)) (Polynomial.map (Int.castRingHom ℚ) (P.Q j))) (F : Fin k → ArithmeticMap 1) (hF : ∀ (j : Fin k) (n : Tuple 1), 0 ≤ F j n) (N : ℕ+) : ∑ n ∈ Finset.Icc 1 N, P.weight (productArithmeticMap F) n ≤ ∏ j : Fin k, ∑ m ∈ Finset.Icc 1 N, (F j fun (x : Fin 1) => m) * (↑(rootCount (P.Q j) ↑m) / ↑↑m)

Factored upper bound for the full dagger weight sum at an integral cutoff.

theorem NairTenenbaum.PolynomialSystem.sum_weight_product_real_le {k r : ℕ} (P : PolynomialSystem k r) (hcop : ∀ (i j : Fin k), i ≠ j → IsCoprime (Polynomial.map (Int.castRingHom ℚ) (P.Q i)) (Polynomial.map (Int.castRingHom ℚ) (P.Q j))) (F : Fin k → ArithmeticMap 1) (hF : ∀ (j : Fin k) (n : Tuple 1), 0 ≤ F j n) (x : ℝ) : ∑ n ∈ positiveUpTo x, P.weight (productArithmeticMap F) n ≤ ∏ j : Fin k, rootWeightedSum (P.Q j) (F j) x

The same bound at every real cutoff, including the empty range below one.

noncomputable def NairTenenbaum.factoredMainTerm {k r : ℕ} (P : PolynomialSystem k r) (F : Fin k → ArithmeticMap 1) (x y : ℝ) : ℝ

Right side of Corollary 3, without the implicit constant.

Equations

• NairTenenbaum.factoredMainTerm P F x y = y * NairTenenbaum.sieveProduct P.total x * ∏ j : Fin k, NairTenenbaum.rootWeightedSum (P.Q j) (F j) x

theorem NairTenenbaum.PolynomialSystem.product_mainTerm_le {k r : ℕ} (P : PolynomialSystem k r) (hcop : ∀ (i j : Fin k), i ≠ j → IsCoprime (Polynomial.map (Int.castRingHom ℚ) (P.Q i)) (Polynomial.map (Int.castRingHom ℚ) (P.Q j))) (F : Fin k → ArithmeticMap 1) (hF : ∀ (j : Fin k) (n : Tuple 1), 0 ≤ F j n) (x : ℝ) {y : ℝ} (hy : 0 ≤ y) : mainTerm P (productArithmeticMap F) x y ≤ factoredMainTerm P F x y