A uniform quantitative base band for actual rough counts

The extra boundary term is essential when x is near y. The unit and possible prime square are retained in the exact formula before estimation.

theorem LiLiuPrereqBuchstab.primeCutoff_le_primeCounting {x y : ℝ} (hx : 0 ≤ x) (hyx : y ≤ x) : ⌈y⌉₊.primeCounting' ≤ ⌊x⌋₊.primeCounting

theorem LiLiuPrereqBuchstab.squareCorrection_le_one (x y : ℝ) : squareCorrection x y ≤ 1

theorem LiLiuPrereqBuchstab.roughCount_le_sq_real {x y : ℝ} (hy : 0 ≤ y) (hx1 : 1 ≤ x) (hyx : y ≤ x) (hxy : x ≤ y ^ 2) : ↑(roughCount x y) = 1 + primePi x - ↑⌈y⌉₊.primeCounting' + ↑(squareCorrection x y)

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

theorem LiLiuPrereqBuchstab.base_log_ratio_mem {x y : ℝ} (hy : 1 < y) (hyx : y ≤ x) (hxy : x ≤ y ^ 2) : 1 ≤ Real.log x / Real.log y ∧ Real.log x / Real.log y ≤ 2

theorem LiLiuPrereqBuchstab.base_buchstab_main_eq {x y : ℝ} (hy : 1 < y) (hyx : y ≤ x) (hxy : x ≤ y ^ 2) : x * buchstab (Real.log x / Real.log y) / Real.log y = x / Real.log x

theorem LiLiuPrereqBuchstab.roughCount_base_buchstab_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| ≤ primeErrorEnvelope y * (x / Real.log y) + 4 * (y / Real.log y)

The K=2 induction estimate, with a constant independent of x and y.