Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiProposition118SourceIntegralDDE

Integral DDE for the genuine Proposition 11.8 source #

This module derives the integral delay equation directly from Suzuki's finite continuous-layer recursion, and then feeds it to the Section-10 Iwaniec pairing. No DDE or pairing conclusion is assumed.

The even source series is the integral primitive of the shifted odd series. This is the infinite-layer form of the finite (9.2) recurrence.

The genuine source is interval-integrable on every compact subinterval of its series range. Measurability comes directly from the two layer tsums; the production hat comparison supplies a continuous compact majorant.

The direct finite-layer argument gives the source integral DDE on every interval 2 ≤ x ≤ y, including intervals crossing the kink at 3.

The shifted source occurring in the DDE is interval-integrable on every compact interval contained in [2,∞).

The weighted source s ↦ sQ(s) is continuous on every compact interval of the series range, directly from its integral DDE.

Consequently the genuine source is continuous at every point strictly above the lower boundary (on the series side of the possible boundary jump).

On the prescribed initial history, the source is continuous away from its endpoints.

The source itself is interval-integrable on compact intervals contained in (1,∞); the single switch point at 2 is harmless.

Away from the unique possible kink s=3, the integral DDE differentiates to the weighted source equation (sQ(s))'=-Q(s-1).