Documentation

MathlibNt.SieveTheory.LinearSieve.JurkatRichert.JurkatRichert1965Section13HatSource

The actual dimension-one Section 13 hat functions #

The positive extensions of -F' / (2 exp γ) and f' / (2 exp γ) give Suzuki's two hat functions. Their source contract is derived from the constructed Jurkat--Richert delay solution, not assumed.

source
noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatPlus (s : ℝ) :
ℝ

Positive extension of the normalized negative upper derivative.

Equations
Instances For
    source
    noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatMinus (s : ℝ) :
    ℝ

    Positive extension of the normalized lower derivative, including its right derivative at the initial endpoint.

    Equations
    Instances For
      source
      noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965Section13HatLayers :
      SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers

      The actual Section 13 data, with β̂ = 2.

      Equations
      Instances For
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatPlus_eq {s : ℝ} (hs : 1 < s) :
        jr1965HatPlus s = (jr1965F s - jr1965f (s - 1)) / (jr1965DelayConstant * s)
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatMinus_eq {s : ℝ} (hs : 2 ≤ s) :
        jr1965HatMinus s = (jr1965F (s - 1) - jr1965f s) / (jr1965DelayConstant * s)
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatPlus_pos {s : ℝ} (hs : 0 < s) :
        0 < jr1965HatPlus s
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatMinus_pos {s : ℝ} (hs : 0 < s) :
        0 < jr1965HatMinus s
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuousOn_jr1965HatPlus :
        ContinuousOn jr1965HatPlus (Set.Ioi 0)
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuousOn_jr1965HatMinus :
        ContinuousOn jr1965HatMinus (Set.Ioi 0)
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_jr1965F_hat {s : ℝ} (hs : 0 < s) :
        HasDerivAt jr1965F (-jr1965DelayConstant * jr1965HatPlus s) s
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_jr1965f_hat {s : ℝ} (hs : 2 < s) :
        HasDerivAt jr1965f (jr1965DelayConstant * jr1965HatMinus s) s
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_weighted_jr1965HatPlus {s : ℝ} (hs : 3 < s) :
        HasDerivAt (fun (x : ℝ) => x ^ 2 * jr1965HatPlus x) (-s * jr1965HatMinus (s - 1)) s
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_weighted_jr1965HatMinus {s : ℝ} (hs : 2 < s) :
        HasDerivAt (fun (x : ℝ) => x ^ 2 * jr1965HatMinus x) (-s * jr1965HatPlus (s - 1)) s
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.abs_jr1965HatPlus_le_exp {s : ℝ} (hs : 2 ≤ s) :
        |jr1965HatPlus s| ≤ Real.exp 2 * (1 + Real.exp 1) * Real.exp (-s)
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.abs_jr1965HatMinus_le_exp {s : ℝ} (hs : 2 ≤ s) :
        |jr1965HatMinus s| ≤ Real.exp 2 * (1 + Real.exp 1) * Real.exp (-s)
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965Section13HatLayers_exponentialDecay :
        SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatExponentialDecay jr1965Section13HatLayers
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.tendsto_weighted_jr1965Section13HatLayers (sign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) :
        Filter.Tendsto (SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat jr1965Section13HatLayers sign) Filter.atTop (nhds 0)
        source
        theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965Section13HatSourceContract :
        SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract jr1965Section13HatLayers

        Unconditional witness of all of Suzuki's source requirements (T1)--(T5).