Contribution estimates from an explicit polynomial-value bound

The scale x need not be the location of the integer interval. This allows an affine substitution to retain the original scale and avoid a new height hypothesis for the substituted coefficients.

theorem NairTenenbaum.PolynomialSystem.value_weight_le_of_value_bound {k r : ℕ} (P : PolynomialSystem k r) {A B σ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hB : 0 ≤ B) (hσ : 0 ≤ σ) {x c : ℝ} (hx : 0 ≤ x) {t : ℤ} (hvalue : ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) : (extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval t (P.Q j)).natAbs) ≤ B * x ^ (c * σ) * F 1

A bound for the total value supplies the pointwise arithmetic growth bound, including the zero-extension cases.

theorem NairTenenbaum.PolynomialSystem.primePowerContribution_le_of_value_bound {k r : ℕ} (P : PolynomialSystem k r) {A B σ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hB : 0 ≤ B) (hσ : 0 ≤ σ) {x c z : ℝ} (hx : 0 ≤ x) (hz : 1 ≤ z) {a b : ℤ} (hab : a ≤ b) (hlevel : z ^ 4 ≤ ↑b - ↑a) (hvalue : ∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) : P.primePowerContribution F z a b ≤ 4 * ↑P.total.natDegree * ↑(max P.total.natDegree (P.badDiscriminant ^ 3)) * B * (↑b - ↑a) * (x ^ (c * σ) / z ^ 2) * F 1

The small-prime exceptional contribution under a value bound.

theorem NairTenenbaum.PolynomialSystem.smoothDivisorContribution_le_of_value_bound {k r : ℕ} (P : PolynomialSystem k r) {A B σ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hB : 0 ≤ B) (hσ : 0 ≤ σ) {x c T : ℝ} (hx : 0 ≤ x) (hT : 0 < T) (s : Finset ℕ) (N : ℕ+) {a b : ℤ} (hab : a ≤ b) (hlevel : ↑↑N ≤ ↑b - ↑a) (hvalue : ∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) : P.smoothDivisorContribution F s N T a b ≤ 2 * smoothDivisorBound P.total.natDegree P.badDiscriminant s * B * (↑b - ↑a) * (x ^ (c * σ) * T ^ (-(1 / 2))) * F 1

The fixed-smoothness exceptional contribution under a value bound.

theorem NairTenenbaum.exists_largeRoughContribution_value_bound {g : ℕ} (hg : 0 < g) {ε A : ℝ} (hε : 0 < ε) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) (hA : 1 ≤ A) (c : ℝ) : ∃ (K : ℝ) (x₀ : ℝ), 0 < K ∧ 1 < x₀ ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (B σ : ℝ) (F : ArithmeticMap k), Admissible A B σ F → 1 ≤ B → 0 < σ → ↑g ^ 2 * σ ≤ 1 / 8 → ∀ (x y : ℝ) (N : ℕ+) (a b : ℤ), x₀ ≤ x → ↑↑N ≤ x ^ (3 * ↑g ^ 2 * ε) → x ^ (4 * ↑g ^ 2 * ε) ≤ y → a ≤ b → y / 2 ≤ ↑b - ↑a → ↑b - ↑a ≤ 2 * y → (∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) → P.smallRoughContribution F N a b (x ^ (↑g * ε / 16)) ≤ K * smallDivisorSieveCost B σ g P.badDiscriminant * mainTerm P F x y

Uniform rough-prefix estimate with the value-growth exponent as an input.

theorem NairTenenbaum.exists_intermediatePrefixContribution_value_bound {g : ℕ} (hg : 0 < g) {ε A c : ℝ} (hε : 0 < ε) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) (hA : 1 ≤ A) (hc : 0 ≤ c) : ∃ (K : ℝ) (x₀ : ℝ) (κ : ℝ) (w₀ : ℝ), 0 < K ∧ 1 < x₀ ∧ 0 < κ ∧ 1 < w₀ ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (B σ : ℝ) (F : ArithmeticMap k), Admissible A B σ F → 1 ≤ B → 0 < σ → ↑g ^ 2 * σ ≤ 1 / 8 → ∀ (x y : ℝ) (N : ℕ+) (a b : ℤ), x₀ ≤ x → ↑↑N ≤ x ^ (3 * ↑g ^ 2 * ε) → x ^ (4 * ↑g ^ 2 * ε) ≤ y → a ≤ b → y / 2 ≤ ↑b - ↑a → ↑b - ↑a ≤ 2 * y → (∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) → P.intermediatePrefixContribution F N (x ^ (3 * ↑g ^ 2 * ε / 2)) w₀ x (↑g * ε / 16) a b ≤ K * smoothTailSieveCost A B κ g P.badDiscriminant * mainTerm P F x y

Uniform intermediate-band estimate under the same value-bound hypothesis.

theorem NairTenenbaum.PolynomialSystem.primePowerContribution_power_saving_of_margin {k r g : ℕ} (P : PolynomialSystem k r) (hdeg : P.total.natDegree = g) {A B σ ε c x y τ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hB : 0 ≤ B) (hσ : 0 ≤ σ) (hε : 0 ≤ ε) (hx : 1 ≤ x) (hmargin : c * σ + τ ≤ ↑g * ε) {a b : ℤ} (hab : a ≤ b) (hlevel : (x ^ (↑g * ε / 2)) ^ 4 ≤ ↑b - ↑a) (hlen : ↑b - ↑a ≤ 2 * y) (hvalue : ∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) : P.primePowerContribution F (x ^ (↑g * ε / 2)) a b ≤ 8 * ↑g * ↑(max g (P.badDiscriminant ^ 3)) * B * y * x ^ (-τ) * F 1

A single growth margin gives a uniform power saving for the prime-power exceptional set, independently of the interval's location.

theorem NairTenenbaum.PolynomialSystem.smoothDivisorContribution_power_saving_of_margin {k r g : ℕ} (P : PolynomialSystem k r) (hdeg : P.total.natDegree = g) {A B σ ε c x y τ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hB : 0 ≤ B) (hσ : 0 ≤ σ) (hx : 1 ≤ x) (hmargin : c * σ + τ ≤ 3 * ↑g * ε / 4) (s : Finset ℕ) (N : ℕ+) {a b : ℤ} (hab : a ≤ b) (hlevel : ↑↑N ≤ ↑b - ↑a) (hlen : ↑b - ↑a ≤ 2 * y) (hvalue : ∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) : P.smoothDivisorContribution F s N (x ^ (3 * ↑g * ε / 2)) a b ≤ 4 * smoothDivisorBound g P.badDiscriminant s * B * y * x ^ (-τ) * F 1

The same growth margin pays the smooth-divisor saving.