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.
Inspect dependencies
MathlibNt.SieveTheory.suzukiProposition118SourceTMinus_weighted_sub · compiled type and proof/definition references.
Above the first odd threshold, the odd source series is the integral primitive of the shifted even source series.
Inspect dependencies
MathlibNt.SieveTheory.suzukiProposition118SourceTPlus_weighted_sub · compiled type and proof/definition references.
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.
Inspect dependencies
MathlibNt.SieveTheory.suzukiProposition118SourceQ_intervalIntegrable · compiled type and proof/definition references.
The direct finite-layer argument gives the source integral DDE on every
interval 2 ≤ x ≤ y, including intervals crossing the kink at 3.
Inspect dependencies
MathlibNt.SieveTheory.suzukiProposition118SourceQ_weighted_sub · compiled type and proof/definition references.
The shifted source occurring in the DDE is interval-integrable on every
compact interval contained in [2,∞).
Inspect dependencies
MathlibNt.SieveTheory.suzukiProposition118SourceQ_shift_intervalIntegrable · compiled type and proof/definition references.
The weighted source s ↦ sQ(s) is continuous on every compact interval
of the series range, directly from its integral DDE.
Inspect dependencies
MathlibNt.SieveTheory.continuousOn_weighted_suzukiProposition118SourceQ · compiled type and proof/definition references.
Consequently the genuine source is continuous at every point strictly above the lower boundary (on the series side of the possible boundary jump).
Inspect dependencies
MathlibNt.SieveTheory.continuousAt_suzukiProposition118SourceQ_of_two_lt · compiled type and proof/definition references.
On the prescribed initial history, the source is continuous away from its endpoints.
Inspect dependencies
MathlibNt.SieveTheory.continuousAt_suzukiProposition118SourceQ_of_one_lt_of_lt_two · compiled type and proof/definition references.
The source itself is interval-integrable on compact intervals contained in
(1,∞); the single switch point at 2 is harmless.
Inspect dependencies
MathlibNt.SieveTheory.suzukiProposition118SourceQ_intervalIntegrable_of_one_lt · compiled type and proof/definition references.
Away from the unique possible kink s=3, the integral DDE differentiates
to the weighted source equation (sQ(s))'=-Q(s-1).
Inspect dependencies
MathlibNt.SieveTheory.hasDerivAt_weighted_suzukiProposition118SourceQ · compiled type and proof/definition references.