noncomputable def LiLiuBuchstabSharp.rationalSeed (n : ℕ) (u : ℝ) : ℝ

An everywhere-continuous rational seed; its relevant domain is [2,3].

Equations

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

theorem LiLiuBuchstabSharp.continuous_rationalSeed (n : ℕ) : Continuous (rationalSeed n)

theorem LiLiuBuchstabSharp.rationalSeed_eq {u : ℝ} (hu : 2 ≤ u) (n : ℕ) : rationalSeed n u = (1 + logLower n (u - 1)) / u

theorem LiLiuBuchstabSharp.rationalSeed_error {u : ℝ} (hu : 2 ≤ u) (hu₃ : u ≤ 3) : 0 ≤ LiLiuPrereqBuchstab.buchstab u - rationalSeed 12 u ∧ LiLiuPrereqBuchstab.buchstab u - rationalSeed 12 u ≤ 1 / 200000000000

This error estimate is uniform in the real parameter, not a finite-point test.

noncomputable def LiLiuBuchstabSharp.rationalStep (a : ℝ) (f : ℝ → ℝ) (u : ℝ) : ℝ

One analytic method-of-steps extension, clamped only outside its use interval.

Equations

• LiLiuBuchstabSharp.rationalStep a f u = (a * f a + ∫ (t : ℝ) in a..max a u, f (t - 1)) / max a u

theorem LiLiuBuchstabSharp.continuous_rationalStep {a : ℝ} (ha : 0 < a) {f : ℝ → ℝ} (hf : Continuous f) : Continuous (rationalStep a f)

noncomputable def LiLiuBuchstabSharp.rationalStage : ℕ → ℝ → ℝ

Exact finite-integral expressions, starting from the twelve-term rational seed. Stage n is used only on [n+2,n+3].

Equations

• LiLiuBuchstabSharp.rationalStage 0 = LiLiuBuchstabSharp.rationalSeed 12
• LiLiuBuchstabSharp.rationalStage n.succ = LiLiuBuchstabSharp.rationalStep (↑n + 3) (LiLiuBuchstabSharp.rationalStage n)

theorem LiLiuBuchstabSharp.continuous_rationalStage (n : ℕ) : Continuous (rationalStage n)

theorem LiLiuBuchstabSharp.rationalStage_error (n : ℕ) {u : ℝ} (hu : ↑n + 2 ≤ u) (hub : u ≤ ↑n + 3) : 0 ≤ LiLiuPrereqBuchstab.buchstab u - rationalStage n u ∧ LiLiuPrereqBuchstab.buchstab u - rationalStage n u ≤ 1 / 200000000000

An unconditional enclosure for the actual Buchstab function, at every stage. No smallness property of a certificate or of Buchstab is an input.

theorem LiLiuBuchstabSharp.buchstab_sharp_window_left_enclosure {u : ℝ} (hu : 17 / 4 ≤ u) (hu₅ : u ≤ 5) : rationalStage 2 u ≤ LiLiuPrereqBuchstab.buchstab u ∧ LiLiuPrereqBuchstab.buchstab u ≤ rationalStage 2 u + 1 / 200000000000

First half of the required starting window: the remaining expression is explicit.

theorem LiLiuBuchstabSharp.buchstab_sharp_window_right_enclosure {u : ℝ} (hu : 5 ≤ u) (hu₅ : u ≤ 21 / 4) : rationalStage 3 u ≤ LiLiuPrereqBuchstab.buchstab u ∧ LiLiuPrereqBuchstab.buchstab u ≤ rationalStage 3 u + 1 / 200000000000

Second half of the required starting window. This is an enclosure, not the sharp bound.