Tail of the upper-source pairing window

The unit-window term tends to zero from the genuine source tail and the scaled Laplace tail of the standard upper adjoint.

theorem MathlibNt.SieveTheory.suzukiUpperSourcePairingWindowTail_of_sourceTail (hP : SuzukiUpperSourcePTail) : SuzukiUpperSourcePairingWindowTail

The moving-window term in the upper-source pairing tends to zero once the source tends to 2; the standard-adjoint scaled tail is supplied by its actual Laplace-integral producer.