Global bounds for the Buchstab function

The global integral equation propagates the interval [1/2, 1] from [1, 2] to every subsequent unit interval.

theorem LiLiuPrereqBuchstab.buchstab_bounds {u : ℝ} (hu : 1 ≤ u) : 1 / 2 ≤ buchstab u ∧ buchstab u ≤ 1

The two-sided bound holds on the entire prescribed domain, without an upper cutoff or an analytic hypothesis.

theorem LiLiuPrereqBuchstab.one_half_le_buchstab {u : ℝ} (hu : 1 ≤ u) : 1 / 2 ≤ buchstab u

theorem LiLiuPrereqBuchstab.buchstab_le_one {u : ℝ} (hu : 1 ≤ u) : buchstab u ≤ 1

theorem LiLiuPrereqBuchstab.buchstab_pos {u : ℝ} (hu : 1 ≤ u) : 0 < buchstab u

theorem LiLiuPrereqBuchstab.buchstab_nonneg {u : ℝ} (hu : 1 ≤ u) : 0 ≤ buchstab u

theorem LiLiuPrereqBuchstab.buchstab_ne_zero {u : ℝ} (hu : 1 ≤ u) : buchstab u ≠ 0

theorem LiLiuPrereqBuchstab.one_div_buchstab_bounds {u : ℝ} (hu : 1 ≤ u) : 1 ≤ 1 / buchstab u ∧ 1 / buchstab u ≤ 2

In particular, the Buchstab factor in a denominator is uniformly safe.

theorem LiLiuPrereqBuchstab.buchstab_eq_log_div {u : ℝ} (hu₂ : 2 ≤ u) (hu₃ : u ≤ 3) : buchstab u = (1 + Real.log (u - 1)) / u

The first delayed interval has the familiar logarithmic formula, including both endpoints.

theorem LiLiuPrereqBuchstab.hasDerivAt_buchstab {u : ℝ} (hu : 2 < u) : HasDerivAt buchstab ((buchstab (u - 1) - buchstab u) / u) u

The derivative form of the Buchstab equation, valid for every u > 2.

theorem LiLiuPrereqBuchstab.deriv_buchstab {u : ℝ} (hu : 2 < u) : deriv buchstab u = (buchstab (u - 1) - buchstab u) / u

theorem LiLiuPrereqBuchstab.abs_deriv_buchstab_le {u : ℝ} (hu : 2 < u) : |deriv buchstab u| ≤ 1 / (2 * u)

The global range bounds give a decaying absolute derivative bound.