Documentation

MathlibNt.SieveTheory.LinearSieve.JurkatRichert.JurkatRichert1965ChenDelayMonotonicity

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

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

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

Equations
Instances For
    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuous_delayDifference (A : ℝ) :
    Continuous (delayDifference A)
    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.delayDifference_initial (A : ℝ) {u : ℝ} (hu : u ≤ 2) :
    delayDifference A u = A
    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_delayDifference (A : ℝ) {u : ℝ} (hu : 2 < u) :
    HasDerivAt (delayDifference A) (-delayDifference A (u - 1) / (u - 1)) u
    source
    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.

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

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

    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f_lt_jr1965F {u : ℝ} (hu : 0 < u) :
    jr1965f u < jr1965F u
    source
    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.

    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_jr1965F {u : ℝ} (hu : 2 < u) :
    HasDerivAt jr1965F ((jr1965f (u - 1) - jr1965F u) / u) u
    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_jr1965f {u : ℝ} (hu : 2 < u) :
    HasDerivAt jr1965f ((jr1965F (u - 1) - jr1965f u) / u) u
    source
    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.

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

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

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

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

    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.deriv_jr1965F_neg {u : ℝ} (hu : 0 < u) :
    deriv jr1965F u < 0
    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.deriv_jr1965f_pos {u : ℝ} (hu : 2 < u) :
    0 < deriv jr1965f u
    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F_le_delayConstant {u : ℝ} (hu : 1 ≤ u) :
    jr1965F u ≤ jr1965DelayConstant
    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f_le_delayConstant {u : ℝ} (hu : 1 ≤ u) :
    jr1965f u ≤ jr1965DelayConstant
    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965g_nonneg (ν : ℕ) {u : ℝ} (hu : 0 < u) :
    0 ≤ jr1965g ν u
    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965g_le_delayConstant (ν : ℕ) {u : ℝ} (hu : 1 ≤ u) :
    jr1965g ν u ≤ jr1965DelayConstant
    source
    theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.abs_jr1965g_le_delayConstant (ν : ℕ) {u : ℝ} (hu : 1 ≤ u) :
    |jr1965g ν u| ≤ jr1965DelayConstant
    source
    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.

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