Covering the fourth class at prime arguments by logarithmic bands

noncomputable def NairTenenbaum.PolynomialSystem.primeIntermediatePrefixContribution {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (N : ℕ+) (X w₀ x u : ℝ) (a b : ℤ) : ℝ

The intermediate-prefix contribution restricted to prime arguments above the scale.

Equations

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

theorem NairTenenbaum.PolynomialSystem.primeIntermediatePrefixContribution_le_bands {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (N : ℕ+) (X w₀ x u : ℝ) (a b : ℤ) (hx : 1 < x) (hw₀ : 1 ≤ w₀) (hu : 0 ≤ u) (hu₁ : u ≤ 1) : ∃ (J : Finset ℕ), (∀ j ∈ J, w₀ < x ^ (2 * (u / 2 ^ (j + 1)))) ∧ P.primeIntermediatePrefixContribution F N X w₀ x u a b ≤ ∑ j ∈ J, P.primeSmoothTailPrefixContribution F N (Finset.Icc 0 ⌊x ^ (2 * (u / 2 ^ (j + 1)))⌋₊) X a b (x ^ (u / 2 ^ (j + 1)))

theorem NairTenenbaum.exists_primeIntermediatePrefixContribution_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 → 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.primeIntermediatePrefixContribution F N (x ^ (3 * ↑g ^ 2 * ε / 2)) w₀ x (↑g * ε / 16) a b ≤ K * primeArgumentTailSieveCost A B κ g P.badDiscriminant * primeMainTerm P F x y