The Jurkat--Richert delay functions by finite method of steps

We construct the weighted functions u F(u) and u f(u) from constant initial data, rather than postulating a delay-equation contract. Each finite approximant is continuous and the approximants stabilize on successively larger half-lines. The harmless cutoffs below extend the weighted functions to the whole real line; the sieve functions themselves are used only on the positive half-line.

The normalization is (5.5), and the integral and differential recurrences are (5.7) and (5.6) of Jurkat--Richert (1965). No asymptotic estimates are asserted.

def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayInitial (A : ℝ) (b : Bool) : ℝ

false selects the upper function; true selects the lower function.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayInitial A b = if b = true then 0 else A

def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayStep (A : ℝ) : ℕ → Bool → ℝ → ℝ

Finite method of steps for the weighted pair. The denominator is truncated only outside the domain of integration, where its value is immaterial.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayStep A 0 x✝¹ x✝ = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayInitial A x✝¹
• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayStep A n.succ x✝¹ x✝ = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayInitial A x✝¹ + ∫ (t : ℝ) in 2..max 2 x✝, MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayStep A n (!x✝¹) (t - 1) / max 1 (t - 1)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayStep_initial (A : ℝ) (n : ℕ) (b : Bool) {u : ℝ} (hu : u ≤ 2) : delayStep A n b u = delayInitial A b

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuous_delayStep (A : ℝ) (n : ℕ) (b : Bool) : Continuous (delayStep A n b)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayStep_succ_eq (A : ℝ) (n : ℕ) (b : Bool) {u : ℝ} (hu : u ≤ ↑n + 2) : delayStep A (n + 1) b u = delayStep A n b u

One more step does not change the solution on the already constructed range.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayStep_eq_of_le (A : ℝ) {n m : ℕ} (hnm : n ≤ m) (b : Bool) {u : ℝ} (hu : u ≤ ↑n + 2) : delayStep A m b u = delayStep A n b u

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayWeight (A : ℝ) (b : Bool) (u : ℝ) : ℝ

A globally defined weighted function, requiring only finitely many integrals at any argument. The ceiling is only a choice of a sufficiently large step.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayWeight A b u = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayStep A ⌈u⌉₊ b u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayWeight_eq_step (A : ℝ) (n : ℕ) (b : Bool) {u : ℝ} (hu : u ≤ ↑n + 2) : delayWeight A b u = delayStep A n b u

Any sufficiently advanced finite step computes the global function exactly.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayWeight_initial (A : ℝ) (b : Bool) {u : ℝ} (hu : u ≤ 2) : delayWeight A b u = delayInitial A b

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuous_delayWeight (A : ℝ) (b : Bool) : Continuous (delayWeight A b)

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayIntegrand (A : ℝ) (b : Bool) (t : ℝ) : ℝ

The globally continuous delayed integrand, including an irrelevant extension to the left of the initial endpoint.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayIntegrand A b t = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayWeight A (!b) (t - 1) / max 1 (t - 1)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuous_delayIntegrand (A : ℝ) (b : Bool) : Continuous (delayIntegrand A b)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayWeight_integral (A : ℝ) (b : Bool) {u : ℝ} (hu : 2 ≤ u) : delayWeight A b u = delayInitial A b + ∫ (t : ℝ) in 2..u, delayIntegrand A b t

The global integral equation, proved by stabilization, not assumed.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayFunction (A : ℝ) (b : Bool) (u : ℝ) : ℝ

The unweighted delay pair with arbitrary initial upper constant.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayFunction A b u = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayWeight A b u / u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.mul_delayFunction (A : ℝ) (b : Bool) {u : ℝ} (hu : u ≠ 0) : u * delayFunction A b u = delayWeight A b u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayFunction_initial (A : ℝ) (b : Bool) {u : ℝ} (hu : u ≤ 2) : delayFunction A b u = delayInitial A b / u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuousOn_delayFunction (A : ℝ) (b : Bool) : ContinuousOn (delayFunction A b) (Set.Ioi 0)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayIntegrand_eq (A : ℝ) (b : Bool) {t : ℝ} (ht : 2 ≤ t) : delayIntegrand A b t = delayFunction A (!b) (t - 1)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayFunction_integral_recurrence (A : ℝ) (b : Bool) {v u : ℝ} (hv : 2 ≤ v) (hvu : v ≤ u) : u * delayFunction A b u = v * delayFunction A b v + ∫ (t : ℝ) in v..u, delayFunction A (!b) (t - 1)

Formula (5.7), for the explicitly constructed pair.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_delayWeight (A : ℝ) (b : Bool) {u : ℝ} (hu : 2 < u) : HasDerivAt (delayWeight A b) (delayFunction A (!b) (u - 1)) u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivWithinAt_delayWeight_two (A : ℝ) (b : Bool) : HasDerivWithinAt (delayWeight A b) (delayFunction A (!b) 1) (Set.Ici 2) 2

The right derivative at the initial endpoint, included in (5.6).

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_mul_delayFunction (A : ℝ) (b : Bool) {u : ℝ} (hu : 2 < u) : HasDerivAt (fun (x : ℝ) => x * delayFunction A b x) (delayFunction A (!b) (u - 1)) u

The literal weighted differential equation (5.6) away from the endpoint.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivWithinAt_mul_delayFunction_two (A : ℝ) (b : Bool) : HasDerivWithinAt (fun (x : ℝ) => x * delayFunction A b x) (delayFunction A (!b) 1) (Set.Ici 2) 2

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayFunction_unique (A : ℝ) (k : Bool → ℝ → ℝ) (hinit : ∀ (b : Bool) (u : ℝ), 0 < u → u ≤ 2 → k b u = delayInitial A b / u) (hint : ∀ (b : Bool) (u : ℝ), 2 ≤ u → u * k b u = delayInitial A b + ∫ (t : ℝ) in 2..u, k (!b) (t - 1)) (b : Bool) (u : ℝ) : 0 < u → k b u = delayFunction A b u

Uniqueness of the integral initial-value problem on the positive half-line. This is a consequence of the construction, not an input to it.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayStep_nonneg {A : ℝ} (hA : 0 ≤ A) (n : ℕ) (b : Bool) (u : ℝ) : 0 ≤ delayStep A n b u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayInitial_le_delayWeight {A : ℝ} (hA : 0 ≤ A) (b : Bool) (u : ℝ) : delayInitial A b ≤ delayWeight A b u

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant : ℝ

The normalization constant from Jurkat--Richert (5.5).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant = 2 * Real.exp Real.eulerMascheroniConstant

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F : ℝ → ℝ

The actual global upper delay function, constructed by finite method of steps. This is not the legacy placeholder sieveFunctionF.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayFunction MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant false

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f : ℝ → ℝ

The actual global lower delay function, constructed by finite method of steps. This is not the legacy placeholder sieveFunctionf.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayFunction MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant true

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F_initial {u : ℝ} (hu : u ≤ 2) : jr1965F u = 2 * Real.exp Real.eulerMascheroniConstant / u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f_initial {u : ℝ} (hu : u ≤ 2) : jr1965f u = 0

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuousOn_jr1965F : ContinuousOn jr1965F (Set.Ioi 0)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuousOn_jr1965f : ContinuousOn jr1965f (Set.Ioi 0)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F_integral_recurrence {v u : ℝ} (hv : 2 ≤ v) (hvu : v ≤ u) : u * jr1965F u = v * jr1965F v + ∫ (t : ℝ) in v..u, jr1965f (t - 1)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f_integral_recurrence {v u : ℝ} (hv : 2 ≤ v) (hvu : v ≤ u) : u * jr1965f u = v * jr1965f v + ∫ (t : ℝ) in v..u, jr1965F (t - 1)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_mul_jr1965F {u : ℝ} (hu : 2 < u) : HasDerivAt (fun (x : ℝ) => x * jr1965F x) (jr1965f (u - 1)) u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_mul_jr1965f {u : ℝ} (hu : 2 < u) : HasDerivAt (fun (x : ℝ) => x * jr1965f x) (jr1965F (u - 1)) u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivWithinAt_mul_jr1965F_two : HasDerivWithinAt (fun (x : ℝ) => x * jr1965F x) (jr1965f 1) (Set.Ici 2) 2

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivWithinAt_mul_jr1965f_two : HasDerivWithinAt (fun (x : ℝ) => x * jr1965f x) (jr1965F 1) (Set.Ici 2) 2

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F_pos {u : ℝ} (hu : 0 < u) : 0 < jr1965F u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f_nonneg {u : ℝ} (hu : 0 < u) : 0 ≤ jr1965f u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F_eq_of_le_three {u : ℝ} (hu : u ≤ 3) : jr1965F u = 2 * Real.exp Real.eulerMascheroniConstant / u

The first extended upper formula, Jurkat--Richert (5.8).

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965g (ν : ℕ) (u : ℝ) : ℝ

The parity-indexed notation (5.14).

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965g ν u = if Even ν then MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F u else MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965g_integral_recurrence (ν : ℕ) {v u : ℝ} (hv : 2 ≤ v) (hvu : v ≤ u) : u * jr1965g ν u = v * jr1965g ν v + ∫ (t : ℝ) in v..u, jr1965g (ν + 1) (t - 1)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuousOn_jr1965g (ν : ℕ) : ContinuousOn (jr1965g ν) (Set.Ioi 0)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_mul_jr1965g (ν : ℕ) {u : ℝ} (hu : 2 < u) : HasDerivAt (fun (x : ℝ) => x * jr1965g ν x) (jr1965g (ν + 1) (u - 1)) u