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.

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

Positive extension of the normalized negative upper derivative.

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatPlus s = if s ≤ 3 then 1 / s ^ 2 else (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F s - MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f (s - 1)) / (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant * s)

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatMinus (s : ℝ) : ℝ

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

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatMinus s = if s ≤ 2 then 2 / s ^ 2 else (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F (s - 1) - MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f s) / (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant * s)

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965Section13HatLayers : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers

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

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965Section13HatLayers = { betaHat := 2, Tplus := MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatPlus, Tminus := MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatMinus }

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatPlus_eq {s : ℝ} (hs : 1 < s) : jr1965HatPlus s = (jr1965F s - jr1965f (s - 1)) / (jr1965DelayConstant * s)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatMinus_eq {s : ℝ} (hs : 2 ≤ s) : jr1965HatMinus s = (jr1965F (s - 1) - jr1965f s) / (jr1965DelayConstant * s)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatPlus_pos {s : ℝ} (hs : 0 < s) : 0 < jr1965HatPlus s

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965HatMinus_pos {s : ℝ} (hs : 0 < s) : 0 < jr1965HatMinus s

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuousOn_jr1965HatPlus : ContinuousOn jr1965HatPlus (Set.Ioi 0)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuousOn_jr1965HatMinus : ContinuousOn jr1965HatMinus (Set.Ioi 0)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_jr1965F_hat {s : ℝ} (hs : 0 < s) : HasDerivAt jr1965F (-jr1965DelayConstant * jr1965HatPlus s) s

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_jr1965f_hat {s : ℝ} (hs : 2 < s) : HasDerivAt jr1965f (jr1965DelayConstant * jr1965HatMinus s) s

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_weighted_jr1965HatPlus {s : ℝ} (hs : 3 < s) : HasDerivAt (fun (x : ℝ) => x ^ 2 * jr1965HatPlus x) (-s * jr1965HatMinus (s - 1)) s

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.hasDerivAt_weighted_jr1965HatMinus {s : ℝ} (hs : 2 < s) : HasDerivAt (fun (x : ℝ) => x ^ 2 * jr1965HatMinus x) (-s * jr1965HatPlus (s - 1)) s

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.abs_jr1965HatPlus_le_exp {s : ℝ} (hs : 2 ≤ s) : |jr1965HatPlus s| ≤ Real.exp 2 * (1 + Real.exp 1) * Real.exp (-s)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.abs_jr1965HatMinus_le_exp {s : ℝ} (hs : 2 ≤ s) : |jr1965HatMinus s| ≤ Real.exp 2 * (1 + Real.exp 1) * Real.exp (-s)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965Section13HatLayers_exponentialDecay : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatExponentialDecay jr1965Section13HatLayers

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.tendsto_weighted_jr1965Section13HatLayers (sign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) : Filter.Tendsto (SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat jr1965Section13HatLayers sign) Filter.atTop (nhds 0)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965Section13HatSourceContract : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract jr1965Section13HatLayers

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