The small-prefix, large-next-prime contribution

This class contains the first class in §4: a prefix of the irreducible value factorization has small weighted mass, and its next-prime cutoff exceeds the sieve bound. No choice of a first crossing prime is built into the class, so its estimate also applies to any such prefix.

def NairTenenbaum.PolynomialSystem.HasSmallRoughPrefix {k r : ℕ} (P : PolynomialSystem k r) (N : ℕ+) (z : ℝ) (t : ℤ) : Prop

A small whole-prime-power prefix with a large cutoff.

Equations

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

noncomputable def NairTenenbaum.PolynomialSystem.smallRoughContribution {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (N : ℕ+) (a b : ℤ) (z : ℝ) : ℝ

The contribution of values admitting a small prefix with a large next-prime cutoff.

Equations

• P.smallRoughContribution F N a b z = ∑ t ∈ Finset.Ioc a b with (P.HasSmallRoughPrefix N z) t, NairTenenbaum.extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval t (P.Q j)).natAbs

theorem NairTenenbaum.PolynomialSystem.smallRoughContribution_le {k r : ℕ} (P : PolynomialSystem k r) {A B σ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hA : 1 ≤ A) (hB : 0 ≤ B) (N : ℕ+) (a b : ℤ) {x α c : ℝ} (hx : 1 < x) (hα : 0 < α) (hvalue : ∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) : P.smallRoughContribution F N a b (x ^ α) ≤ A ^ (c / α) * P.smallDivisorSiftedSum F N a b (x ^ α)

The first-contribution reduction, with all counting and roughness inputs proved and only a total-value upper bound remaining as a hypothesis.