Exponential coalescence of the actual Jurkat--Richert delay pair

The Dickman renewal identity gives an exponential bound for the weighted gap. Monotonicity then supplies a common limit with the same rate. This module does not identify that limit with 1; that normalization is a separate obligation in the proof of (5.10). No asymptotic estimate is assumed.

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

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.mul_delayDifference_le_previous {A u : ℝ} (hA : 0 < A) (hu : 2 ≤ u) : (u - 1) * delayDifference A u ≤ delayDifference A (u - 1)

The renewal average is bounded by its left endpoint.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.antitoneOn_exp_mul_delayDifference {A : ℝ} (hA : 0 < A) : AntitoneOn (fun (u : ℝ) => Real.exp u * delayDifference A u) (Set.Ici 2)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayDifference_le_exp {A u : ℝ} (hA : 0 < A) : delayDifference A u ≤ A * Real.exp 2 * Real.exp (-u)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F_sub_jr1965f_le_exp {u : ℝ} (hu : 1 ≤ u) : jr1965F u - jr1965f u ≤ jr1965DelayConstant * Real.exp 2 * Real.exp (-u)

One constant controls the upper/lower gap on the entire source range.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965CommonLimit : ℝ

The common limit is constructed from the lower function, not postulated.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965CommonLimit = sSup (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f '' Set.Ici 1)

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

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

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.abs_jr1965F_sub_commonLimit_le_exp {u : ℝ} (hu : 1 ≤ u) : |jr1965F u - jr1965CommonLimit| ≤ jr1965DelayConstant * Real.exp 2 * Real.exp (-u)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.abs_jr1965f_sub_commonLimit_le_exp {u : ℝ} (hu : 1 ≤ u) : |jr1965f u - jr1965CommonLimit| ≤ jr1965DelayConstant * Real.exp 2 * Real.exp (-u)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.tendsto_jr1965F_commonLimit : Filter.Tendsto jr1965F Filter.atTop (nhds jr1965CommonLimit)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.tendsto_jr1965f_commonLimit : Filter.Tendsto jr1965f Filter.atTop (nhds jr1965CommonLimit)