The global Buchstab delay function

Continuous integral approximants stabilize on successively larger half-lines. Their locally stable value defines a function on all of ℝ; on [1, ∞) it satisfies the initial condition and the Buchstab delay differential equation. The extension below 1 is only used to keep the approximants globally continuous.

noncomputable def LiLiuPrereqBuchstab.approx : ℕ → ℝ → ℝ

The method-of-steps approximants, with harmless continuous cutoffs below the interval on which the Buchstab equation is prescribed.

Equations

• LiLiuPrereqBuchstab.approx 0 x✝ = 1 / max 1 x✝
• LiLiuPrereqBuchstab.approx n.succ x✝ = (1 + ∫ (t : ℝ) in 2..max 2 x✝, LiLiuPrereqBuchstab.approx n (t - 1)) / max 1 x✝

theorem LiLiuPrereqBuchstab.continuous_approx (n : ℕ) : Continuous (approx n)

theorem LiLiuPrereqBuchstab.approx_succ_eq (n : ℕ) (u : ℝ) (hu : u ≤ ↑n + 2) : approx (n + 1) u = approx n u

One more integral step makes no change below its stabilization threshold.

theorem LiLiuPrereqBuchstab.approx_eq_of_le {n m : ℕ} (hnm : n ≤ m) (u : ℝ) (hu : u ≤ ↑n + 2) : approx m u = approx n u

Any later approximant agrees on the earlier stabilization half-line.

noncomputable def LiLiuPrereqBuchstab.buchstab (u : ℝ) : ℝ

The actual global Buchstab function, obtained by locally stabilized method-of-steps approximants, rather than a fixed finite truncation.

Equations

• LiLiuPrereqBuchstab.buchstab u = LiLiuPrereqBuchstab.approx ⌈u⌉₊ u

theorem LiLiuPrereqBuchstab.buchstab_eq_approx (n : ℕ) (u : ℝ) (hu : u ≤ ↑n + 2) : buchstab u = approx n u

theorem LiLiuPrereqBuchstab.buchstab_eventuallyEq_approx (n : ℕ) (u : ℝ) (hu : u < ↑n + 2) : buchstab =ᶠ[nhds u] approx n

Locally the glued function is a single continuous approximant.

theorem LiLiuPrereqBuchstab.continuous_buchstab : Continuous buchstab

theorem LiLiuPrereqBuchstab.continuousOn_buchstab : ContinuousOn buchstab (Set.Ici 1)

theorem LiLiuPrereqBuchstab.buchstab_eq_one_div {u : ℝ} (hu₁ : 1 ≤ u) (hu₂ : u ≤ 2) : buchstab u = 1 / u

The prescribed initial condition, including both endpoints.

theorem LiLiuPrereqBuchstab.mul_buchstab_eq_integral {u : ℝ} (hu : 2 ≤ u) : u * buchstab u = 1 + ∫ (t : ℝ) in 2..u, buchstab (t - 1)

The global integral equation; there is no upper bound on u.

theorem LiLiuPrereqBuchstab.hasDerivAt_mul_buchstab {u : ℝ} (hu : 2 < u) : HasDerivAt (fun (v : ℝ) => v * buchstab v) (buchstab (u - 1)) u

The Buchstab delay differential equation at every real u > 2.