Documentation

MathlibNt.SieveTheory.LinearSieve.JurkatRichert.JurkatRichert1965ChenDelayDecay

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.

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

MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.antitone_delayDifference · compiled type and proof/definition references.

source
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.

Inspect dependencies

MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.mul_delayDifference_le_previous · compiled type and proof/definition references.

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

MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.antitoneOn_exp_mul_delayDifference · compiled type and proof/definition references.

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

MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayDifference_le_exp · compiled type and proof/definition references.

source
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.

Inspect dependencies

MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F_sub_jr1965f_le_exp · compiled type and proof/definition references.

source
noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965CommonLimit :
ℝ

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

Equations
Instances For
    Inspect dependencies

    MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965CommonLimit · compiled type and proof/definition references.

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

    MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f_le_commonLimit · compiled type and proof/definition references.

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

    MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.commonLimit_le_jr1965F · compiled type and proof/definition references.

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

    MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.abs_jr1965F_sub_commonLimit_le_exp · compiled type and proof/definition references.

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

    MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.abs_jr1965f_sub_commonLimit_le_exp · compiled type and proof/definition references.

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

    MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.tendsto_jr1965F_commonLimit · compiled type and proof/definition references.

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

    MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.tendsto_jr1965f_commonLimit · compiled type and proof/definition references.