The small-prefix contribution at prime arguments

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

The small-prefix contribution restricted to prime arguments above the sieve cutoff.

Equations

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

theorem NairTenenbaum.PolynomialSystem.primeSmallRoughContribution_le {k r : ℕ} (P : PolynomialSystem k r) {A B σ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hA : 1 ≤ A) (hB : 0 ≤ B) (g : ℕ) (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.primeSmallRoughContribution F N a b (x ^ α) ≤ A ^ (c / α) * P.primeSmallDivisorSiftedSum F g 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.

theorem NairTenenbaum.exists_primeSmallRoughContribution_mainTerm_bound {g : ℕ} (hg : 0 < g) {ε A c : ℝ} (hε : 0 < ε) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) (hA : 1 ≤ A) : ∃ (K : ℝ) (x₀ : ℝ), 0 < K ∧ 1 < x₀ ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → Polynomial.eval 0 P.total ≠ 0 → ∀ (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.primeSmallRoughContribution F N a b (x ^ (↑g * ε / 16)) ≤ K * primeArgumentSmallSieveCost B σ g P.badDiscriminant * primeMainTerm P F x y

Uniform control of the first class with the logarithmic saving. Only values of the original total polynomial enter the pointwise growth bound.