The exact Buchstab logarithmic integral

The primitive -(L / log t) * buchstab (L / log t) / L evaluates the logarithmic kernel. The fundamental theorem is used only on the interior: the upper endpoint, where the Buchstab argument is 2, needs continuity but not differentiability. In particular the square endpoint is included.

theorem LiLiuPrereqBuchstab.hasDerivAt_buchstab_log_primitive {L t : ℝ} (ht : 1 < t) (hLt : 2 < L / Real.log t) : HasDerivAt (fun (s : ℝ) => -(L / Real.log s * buchstab (L / Real.log s)) / L) (buchstab (L / Real.log t - 1) / (t * Real.log t ^ 2)) t

The antiderivative of the logarithmic Buchstab kernel, away from the initial-condition corner.

theorem LiLiuPrereqBuchstab.intervalIntegrable_buchstab_log_kernel {a b : ℝ} (L : ℝ) (ha : 1 < a) (hab : a ≤ b) : IntervalIntegrable (fun (t : ℝ) => buchstab (L / Real.log t - 1) / (t * Real.log t ^ 2)) MeasureTheory.volume a b

The logarithmic kernel is integrable on every compact interval above 1.

theorem LiLiuPrereqBuchstab.integral_buchstab_log_kernel {a b L : ℝ} (ha : 1 < a) (hab : a ≤ b) (hLb : L / Real.log b = 2) : ∫ (t : ℝ) in a..b, buchstab (L / Real.log t - 1) / (t * Real.log t ^ 2) = (L / Real.log a * buchstab (L / Real.log a) - 1) / L

Exact evaluation with an arbitrary logarithmic numerator and an upper endpoint whose transformed value is 2. The interval may be degenerate.

theorem LiLiuPrereqBuchstab.integral_buchstab_log_substitution {a b L : ℝ} (ha : 1 < a) (hab : a ≤ b) (hLb : L / Real.log b = 2) : ∫ (t : ℝ) in a..b, buchstab (L / Real.log t - 1) / (t * Real.log t ^ 2) = (∫ (v : ℝ) in 2..L / Real.log a, buchstab (v - 1)) / L

The corresponding exact change of variable v = L / log t.

theorem LiLiuPrereqBuchstab.log_div_log_sqrt {x : ℝ} (hx : 1 < x) : Real.log x / Real.log √x = 2

The upper logarithmic endpoint is exactly 2, not merely asymptotic.

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

The square-cutoff hypothesis places the lower transformed endpoint in the domain of the Buchstab integral equation, including equality at 2.

theorem LiLiuPrereqBuchstab.integral_buchstab_log_kernel_sqrt {x y : ℝ} (hy : 1 < y) (hxy : y ^ 2 ≤ x) : ∫ (t : ℝ) in y..√x, buchstab (Real.log x / Real.log t - 1) / (t * Real.log t ^ 2) = (Real.log x / Real.log y * buchstab (Real.log x / Real.log y) - 1) / Real.log x

Exact unscaled evaluation on the interval from y to sqrt x.

theorem LiLiuPrereqBuchstab.mul_integral_buchstab_log_kernel_sqrt {x y : ℝ} (hy : 1 < y) (hxy : y ^ 2 ≤ x) : x * ∫ (t : ℝ) in y..√x, buchstab (Real.log x / Real.log t - 1) / (t * Real.log t ^ 2) = x / Real.log x * (Real.log x / Real.log y * buchstab (Real.log x / Real.log y) - 1)

Identity (I) in the compact-uniform rough-count argument. Both real endpoints are exact, and x = y² is allowed.