noncomputable def LiLiuBuchstabSharp.logLower (n : ℕ) (x : ℝ) : ℝ

The finite odd-power expansion used below is algebraic, not sampled data.

Equations

• LiLiuBuchstabSharp.logLower n x = 2 * ∑ i ∈ Finset.range n, ((x - 1) / (x + 1)) ^ (2 * i + 1) / (2 * ↑i + 1)

theorem LiLiuBuchstabSharp.logLower_error {x : ℝ} (hx : 1 ≤ x) (hx₂ : x ≤ 2) (n : ℕ) : 0 ≤ Real.log x - logLower n x ∧ Real.log x - logLower n x ≤ 9 / 4 * (1 / 3) ^ (2 * n + 1)

A uniform, explicitly bounded analytic remainder on the complete interval [1,2].

theorem LiLiuBuchstabSharp.logLower_twelve_error {x : ℝ} (hx : 1 ≤ x) (hx₂ : x ≤ 2) : 0 ≤ Real.log x - logLower 12 x ∧ Real.log x - logLower 12 x < 1 / 100000000000

Twelve exact Taylor terms give a uniform error strictly below 10⁻¹¹.

theorem LiLiuBuchstabSharp.buchstab_le_709_div_1250 {u : ℝ} (hu : 2 ≤ u) : LiLiuPrereqBuchstab.buchstab u ≤ 709 / 1250

An unconditional improvement of the previous coarse bound. This is NOT the requested sharp decimal bound.