Finite-band estimates for the actual rough-integer count

The error function is constructed from the actual PNT envelope. Constants are independent of both real parameters, and the boundary term retains the unit when the two parameters are close.

noncomputable def LiLiuPrereqBuchstab.buchstabRemainder (y : ℝ) : ℝ

Equations

• LiLiuPrereqBuchstab.buchstabRemainder y = LiLiuPrereqBuchstab.primeErrorEnvelope y + 1 / Real.log y

theorem LiLiuPrereqBuchstab.buchstabRemainder_nonneg {y : ℝ} (hy : primeErrorStart ≤ y) : 0 ≤ buchstabRemainder y

theorem LiLiuPrereqBuchstab.antitoneOn_buchstabRemainder : AntitoneOn buchstabRemainder (Set.Ici primeErrorStart)

theorem LiLiuPrereqBuchstab.tendsto_buchstabRemainder : Filter.Tendsto buchstabRemainder Filter.atTop (nhds 0)

theorem LiLiuPrereqBuchstab.buchstabRemainder_inv_log_le {y : ℝ} : 1 / Real.log y ≤ buchstabRemainder y

theorem LiLiuPrereqBuchstab.buchstabRemainder_envelope_le {y : ℝ} (hy : primeErrorStart ≤ y) : primeErrorEnvelope y ≤ buchstabRemainder y

theorem LiLiuPrereqBuchstab.buchstabRemainder_log_sq_bound {x y : ℝ} (hy : primeErrorStart ≤ y) (hx : 0 ≤ x) : x / Real.log y ^ 2 ≤ buchstabRemainder y * (x / Real.log y)

theorem LiLiuPrereqBuchstab.sievingPrimes_sqrt_eq_primesIco {x y : ℝ} (hx : 1 ≤ x) : sievingPrimes x y √x = primesIco y √x

theorem LiLiuPrereqBuchstab.roughCount_buchstab_sqrt {x y : ℝ} (hx : 1 ≤ x) (hy : y ≤ √x) : ↑(roughCount x y) = ↑(roughCount x √x) + ∑ p ∈ primesIco y √x, ↑(roughCount (x / ↑p) ↑p)

theorem LiLiuPrereqBuchstab.buchstabPrimeKernel_eq_subproblem {x p : ℝ} (hx : 0 < x) (hp : 1 < p) : buchstabPrimeKernel x p = x / p * buchstab (Real.log (x / p) / Real.log p) / Real.log p

theorem LiLiuPrereqBuchstab.sum_primesIco_inv_mul_log_le {y b : ℝ} (hy : primeErrorStart ≤ y) (hyb : y ≤ b) : ∑ p ∈ primesIco y b, 1 / (↑p * Real.log ↑p) ≤ 5 / Real.log y

theorem LiLiuPrereqBuchstab.sum_primesIco_div_log_le {y b : ℝ} (hy : primeErrorStart ≤ y) (hyb : y ≤ b) : ∑ p ∈ primesIco y b, ↑p / Real.log ↑p ≤ 2 * b ^ 2 / Real.log b ^ 2

theorem LiLiuPrereqBuchstab.roughCount_sqrt_error_le {x y : ℝ} (hy : primeErrorStart ≤ y) (hxy : y ^ 2 ≤ x) : |↑(roughCount x √x) - x / Real.log x| ≤ 5 * (buchstabRemainder y * (x / Real.log y))

The square-root terminal count costs only five copies of the common error.

theorem LiLiuPrereqBuchstab.sum_buchstabRemainder_errors_le {x y : ℝ} (hy : primeErrorStart ≤ y) (hxy : y ^ 2 ≤ x) : ∑ p ∈ primesIco y √x, (buchstabRemainder ↑p * (x / ↑p / Real.log ↑p) + ↑p / Real.log ↑p) ≤ 7 * (buchstabRemainder y * (x / Real.log y))

Summing the recursively generated errors has the uniform multiplier seven.

theorem LiLiuPrereqBuchstab.buchstab_subproblem_band {x y : ℝ} {k p : ℕ} (hy : primeErrorStart ≤ y) (hxy : x ≤ y ^ (k + 1)) (hp : p ∈ primesIco y √x) : primeErrorStart ≤ ↑p ∧ ↑p ≤ x / ↑p ∧ x / ↑p ≤ ↑p ^ k

theorem LiLiuPrereqBuchstab.log_ratio_le_of_le_pow {x y : ℝ} {k : ℕ} (hy : primeErrorStart ≤ y) (hyx : y ≤ x) (hxy : x ≤ y ^ k) : Real.log x / Real.log y ≤ ↑k

def LiLiuPrereqBuchstab.buchstabBandConstant (k : ℕ) : ℝ

An explicit finite-band constant, depending only on the integer band.

Equations

• LiLiuPrereqBuchstab.buchstabBandConstant k = 112 * 8 ^ k

theorem LiLiuPrereqBuchstab.buchstabBandConstant_ge (k : ℕ) : 112 ≤ buchstabBandConstant k

theorem LiLiuPrereqBuchstab.buchstabBandConstant_succ (k : ℕ) : buchstabBandConstant (k + 1) = 8 * buchstabBandConstant k

theorem LiLiuPrereqBuchstab.roughCount_base_remainder_error {x y : ℝ} (hy : primeErrorStart ≤ y) (hyx : y ≤ x) (hxy : x ≤ y ^ 2) : |↑(roughCount x y) - x * buchstab (Real.log x / Real.log y) / Real.log y| ≤ 4 * (buchstabRemainder y * (x / Real.log y) + y / Real.log y)

theorem LiLiuPrereqBuchstab.roughCount_buchstab_band_error (k : ℕ) (hk : k ≤ 100) {x y : ℝ} (hy : primeErrorStart ≤ y) (hyx : y ≤ x) (hxy : x ≤ y ^ k) : |↑(roughCount x y) - x * buchstab (Real.log x / Real.log y) / Real.log y| ≤ buchstabBandConstant k * (buchstabRemainder y * (x / Real.log y) + y / Real.log y)

The actual finite-band induction, with no rough-count estimate among its hypotheses. The same explicit constant works for all real x,y in the band.

theorem LiLiuPrereqBuchstab.roughCount_buchstab_band_100 : ∃ (C : ℝ), 0 < C ∧ ∀ (x y : ℝ), primeErrorStart ≤ y → y ≤ x → x ≤ y ^ 100 → |↑(roughCount x y) - x * buchstab (Real.log x / Real.log y) / Real.log y| ≤ C * (buchstabRemainder y * (x / Real.log y) + y / Real.log y)

In particular, there is one constant for the entire band through 100.