Order properties of the constructed Jurkat--Richert delay functions

The weighted difference satisfies the Dickman renewal identity. Its positivity gives the order and monotonicity statements in Jurkat--Richert (1965), (5.11)--(5.13).

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayDifference (A u : ℝ) : ℝ

The weighted upper-minus-lower difference of the actual finite-step solution.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayDifference A u = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayWeight A false u - MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayWeight A true u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuous_delayDifference (A : ℝ) : Continuous (delayDifference A)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayDifference_initial (A : ℝ) {u : ℝ} (hu : u ≤ 2) : delayDifference A u = A

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_delayDifference (A : ℝ) {u : ℝ} (hu : 2 < u) : HasDerivAt (delayDifference A) (-delayDifference A (u - 1) / (u - 1)) u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayDifference_renewal (A : ℝ) {u : ℝ} (hu : 2 ≤ u) : (u - 1) * delayDifference A u = ∫ (t : ℝ) in u - 1..u, delayDifference A t

The renewal identity, including its initial endpoint.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayDifference_pos {A : ℝ} (hA : 0 < A) (u : ℝ) : 0 < delayDifference A u

Strict positivity of the weighted difference, by its renewal identity.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayFunction_lower_lt_upper {A u : ℝ} (hA : 0 < A) (hu : 0 < u) : delayFunction A true u < delayFunction A false u

The strict gap (5.11), for the constructed pair and positive normalization.

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

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

The unweighted differential equation on the open delay range.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_jr1965F {u : ℝ} (hu : 2 < u) : HasDerivAt jr1965F ((jr1965f (u - 1) - jr1965F u) / u) u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_jr1965f {u : ℝ} (hu : 2 < u) : HasDerivAt jr1965f ((jr1965F (u - 1) - jr1965f u) / u) u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f_sub_one_lt_jr1965F {u : ℝ} (hu : 2 ≤ u) : jr1965f (u - 1) < jr1965F u

The delayed lower function stays strictly below the current upper function. At a first failure, the upper function is decreasing up to that point, hence the lower one is increasing, contradicting the strict upper/lower gap.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.antitoneOn_jr1965F : AntitoneOn jr1965F (Set.Ioi 0)

The upper function is decreasing on the entire positive half-line.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.monotoneOn_jr1965f : MonotoneOn jr1965f (Set.Ioi 0)

The lower function is increasing on the entire positive half-line.

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

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.deriv_jr1965f_pos {u : ℝ} (hu : 2 < u) : 0 < deriv jr1965f u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F_le_delayConstant {u : ℝ} (hu : 1 ≤ u) : jr1965F u ≤ jr1965DelayConstant

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f_le_delayConstant {u : ℝ} (hu : 1 ≤ u) : jr1965f u ≤ jr1965DelayConstant

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965g_nonneg (ν : ℕ) {u : ℝ} (hu : 0 < u) : 0 ≤ jr1965g ν u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965g_le_delayConstant (ν : ℕ) {u : ℝ} (hu : 1 ≤ u) : jr1965g ν u ≤ jr1965DelayConstant

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.abs_jr1965g_le_delayConstant (ν : ℕ) {u : ℝ} (hu : 1 ≤ u) : |jr1965g ν u| ≤ jr1965DelayConstant

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.eVariationOn_jr1965g_Ici_le (ν : ℕ) : eVariationOn (jr1965g ν) (Set.Ici 1) ≤ ENNReal.ofReal jr1965DelayConstant

Uniform total variation on the entire unbounded sieve range. In particular, the bound does not depend on either endpoint of a finite subinterval.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.boundedVariationOn_jr1965g_Ici (ν : ℕ) : BoundedVariationOn (jr1965g ν) (Set.Ici 1)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.eVariationOn_jr1965g_Icc_le (ν : ℕ) {a b : ℝ} (ha : 1 ≤ a) : eVariationOn (jr1965g ν) (Set.Icc a b) ≤ ENNReal.ofReal jr1965DelayConstant