Pairing conservation directly from an integral delay equation

This module avoids differentiating the source function at the left endpoint. The integral DDE itself supplies the required right derivative, including at x = 2, where only right continuity of the delayed value at 1 is used.

noncomputable def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.sourceWeightedPairing (F : ℝ → ℝ) (s : ℝ) : ℝ

The κ=1 Iwaniec pairing in weighted coordinates F(s) = s Q(s).

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.sourceWeightedPairing F s = (s - 1) * F s - ∫ (t : ℝ) in s - 1..s, F t

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.sourceWeightedPairing_eq_of_integralDDE {F : ℝ → ℝ} (hF : ContinuousOn F (Set.Ici 1)) (hDDE : ∀ (a b : ℝ), 2 ≤ a → a ≤ b → F b - F a = -∫ (t : ℝ) in a..b, F (t - 1) / (t - 1)) {x y : ℝ} (hx : 2 ≤ x) (hxy : x ≤ y) : sourceWeightedPairing F y = sourceWeightedPairing F x

An integral delay equation conserves the κ=1 Iwaniec pairing. Crucially, F is assumed continuous only on [1,∞), and the equation is used only in forward form on [2,∞). Thus the theorem includes x = 2 without any left-continuity hypothesis at the threshold.