Jurkat--Richert (5.10) for the constructed global delay functions

The common limit is 1: pair the actual sum F + f with the independently constructed Laplace adjoint. The conserved pairing is 2 at the initial endpoint and twice the common limit at infinity.

This is a modern adjoint proof of the exact statement on printed p. 226, not the original paper's appeal to de Bruijn's estimates (5.3). Only the generic pairing identity and unconditional adjoint producers are reused; no Suzuki source-tail or amplitude-normalization hypothesis is consumed.

noncomputable def MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelaySum (u : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelaySum u = MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F u + MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.continuousOn_jr1965DelaySum : ContinuousOn jr1965DelaySum (Set.Ici 1)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelaySum_initial {u : ℝ} (hu : u ≤ 2) : jr1965DelaySum u = jr1965DelayConstant / u

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelaySum_integral_recurrence (a b : ℝ) (ha : 2 ≤ a) (hab : a ≤ b) : b * jr1965DelaySum b - a * jr1965DelaySum a = ∫ (t : ℝ) in a..b, jr1965DelaySum (t - 1)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.norm_jr1965DelaySum_le {u : ℝ} (hu : 1 ≤ u) : ‖jr1965DelaySum u‖ ≤ 2 * jr1965DelayConstant

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelaySum_adjoint_pairing_two : upperSourcePairingFor jr1965DelaySum suzukiStandardUpperAdjoint 2 = 2

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelaySum_adjoint_pairing_eq_two {u : ℝ} (hu : 2 ≤ u) : upperSourcePairingFor jr1965DelaySum suzukiStandardUpperAdjoint u = 2

The generic conservation theorem instantiated on the actual JR functions.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.tendsto_jr1965DelaySum_adjoint_window : Filter.Tendsto (fun (s : ℝ) => ∫ (t : ℝ) in s - 1..s, suzukiStandardUpperAdjoint (t + 1) * jr1965DelaySum t) Filter.atTop (nhds 0)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965CommonLimit_eq_one : jr1965CommonLimit = 1

The initial amplitude 2 exp gamma gives common limit 1, proved by an independent adjoint identity rather than supplied as an asymptotic premise.

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

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

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

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

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.exists_jr1965_delay_asymptotic : ∃ A > 0, ∀ (u : ℝ), 1 ≤ u → |jr1965F u - 1| ≤ A * Real.exp (-u) ∧ |jr1965f u - 1| ≤ A * Real.exp (-u)

Literal quantified (5.10): one positive constant, both functions, all u >= 1.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.abs_jr1965g_sub_one_le_exp (ν : ℕ) {u : ℝ} (hu : 1 ≤ u) : |jr1965g ν u - 1| ≤ jr1965DelayConstant * Real.exp 2 * Real.exp (-u)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.tendsto_jr1965F_one : Filter.Tendsto jr1965F Filter.atTop (nhds 1)

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.tendsto_jr1965f_one : Filter.Tendsto jr1965f Filter.atTop (nhds 1)