The contribution of a smooth prefix with a rough remainder

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

A whole-prime-power prefix whose weighted mass lies in (X,N], is supported on s, and whose remaining prime factors exceed z.

Equations

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

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

The contribution of smooth prefixes above the combined mass cutoff.

Equations

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

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

The contribution uses existence of a suitable prefix and does not depend on any particular choice of witnesses.

theorem NairTenenbaum.exists_primeBandContribution_mainTerm_bound {g : ℕ} (hg : 0 < g) {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℝ) (x₀ : ℝ), 0 < K ∧ 1 ≤ x₀ ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (A B σ κ c : ℝ) (F : ArithmeticMap k), Admissible A B σ F → 1 ≤ A → 1 ≤ B → 0 < σ → 0 ≤ κ → ↑g ^ 2 * σ ≤ 1 / 8 → c * Real.log A + 4 * ↑g * Real.log 4 + 1 ≤ κ * (3 * ↑g ^ 2 * ε / 2) / 2 → ∀ (x y α : ℝ) (N : ℕ+) (a b : ℤ), x₀ ≤ x → 1 < x → 1 ≤ Real.log x → 0 < α → 2 * α ≤ 1 → α ≤ ↑g * ε / 16 → 2 ≤ x ^ α → 2 * ↑g ≤ x ^ α → 16 ≤ Real.log (x ^ α) → 8 * ↑g ^ 2 * κ ≤ Real.log (x ^ (2 * α)) → ↑↑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.smoothTailPrefixContribution F N (Finset.Icc 0 ⌊x ^ (2 * α)⌋₊) (x ^ (3 * ↑g ^ 2 * ε / 2)) a b (x ^ α) ≤ K * smoothTailSieveCost A B κ g P.badDiscriminant * Real.exp (-1 / α) * mainTerm P F x y

Uniform one-band bound for the original arithmetic weights, rather than just the selected divisor weights.