Unconditional upper-source pairing conservation route

This module separates the two genuine analytic producers still missing from the upper source construction: its forward integral DDE and its tail P(s) → 2. It proves the Iwaniec pairing is constant on [2,∞) from the integral DDE and the standard-adjoint DDE, without using Proposition 11.8(iii).

def MathlibNt.SieveTheory.SuzukiUpperSourcePIntegralDDE : Prop

Exact forward integral DDE required of the already-defined genuine upper source. This is an independently producible source-series theorem.

Equations

• MathlibNt.SieveTheory.SuzukiUpperSourcePIntegralDDE = (ContinuousOn MathlibNt.SieveTheory.suzukiUpperSourceP (Set.Ici 1) ∧ ∀ (a b : ℝ), 2 ≤ a → a ≤ b → b * MathlibNt.SieveTheory.suzukiUpperSourceP b - a * MathlibNt.SieveTheory.suzukiUpperSourceP a = ∫ (t : ℝ) in a..b, MathlibNt.SieveTheory.suzukiUpperSourceP (t - 1))

def MathlibNt.SieveTheory.SuzukiUpperSourcePTail : Prop

Exact, independent tail target for the genuine upper source.

Equations

• MathlibNt.SieveTheory.SuzukiUpperSourcePTail = Filter.Tendsto MathlibNt.SieveTheory.suzukiUpperSourceP Filter.atTop (nhds 2)

def MathlibNt.SieveTheory.SuzukiStandardUpperAdjointDDE : Prop

The differential identity required from the Laplace-integral standard adjoint. It does not include any pairing normalization.

Equations

• MathlibNt.SieveTheory.SuzukiStandardUpperAdjointDDE = ∀ (s : ℝ), 2 ≤ s → HasDerivAt MathlibNt.SieveTheory.suzukiStandardUpperAdjoint (-MathlibNt.SieveTheory.suzukiStandardUpperAdjoint (s + 1) / s) s

def MathlibNt.SieveTheory.SuzukiUpperSourcePairingWindowTail : Prop

The residual moving-window estimate. It is isolated from both the source DDE and Proposition 11.8; analytically it follows from the two pointwise tails and local continuity.

Equations

• MathlibNt.SieveTheory.SuzukiUpperSourcePairingWindowTail = Filter.Tendsto (fun (s : ℝ) => ∫ (t : ℝ) in s - 1..s, MathlibNt.SieveTheory.suzukiStandardUpperAdjoint (t + 1) * MathlibNt.SieveTheory.suzukiUpperSourceP t) Filter.atTop (nhds 0)

noncomputable def MathlibNt.SieveTheory.upperSourcePairingFor (P p : ℝ → ℝ) (s : ℝ) : ℝ

The same pairing formula with the source exposed as an argument.

Equations

• MathlibNt.SieveTheory.upperSourcePairingFor P p s = s * p s * P s + ∫ (t : ℝ) in s - 1..s, p (t + 1) * P t

theorem MathlibNt.SieveTheory.upperSourcePairing_eq_of_integralDDE {P p : ℝ → ℝ} (hP : ContinuousOn P (Set.Ici 1)) (hDDE : ∀ (a b : ℝ), 2 ≤ a → a ≤ b → b * P b - a * P a = ∫ (t : ℝ) in a..b, P (t - 1)) (hp : ∀ (s : ℝ), 2 ≤ s → HasDerivAt p (-p (s + 1) / s) s) {x y : ℝ} (hx : 2 ≤ x) (hxy : x ≤ y) : upperSourcePairingFor P p y = upperSourcePairingFor P p x

Pairing conservation from a forward integral DDE. The one-sided derivative at 2 is extracted from the integral equation, so no derivative of P is assumed at the switching point.

@[simp]

theorem MathlibNt.SieveTheory.upperSourcePairingFor_actual (p : ℝ → ℝ) (s : ℝ) : upperSourcePairingFor suzukiUpperSourceP p s = suzukiUpperSourcePairing p s

theorem MathlibNt.SieveTheory.suzukiUpperSourcePairing_eq_of_productionDDE (hP : SuzukiUpperSourcePIntegralDDE) (hp : SuzukiStandardUpperAdjointDDE) {x y : ℝ} (hx : 2 ≤ x) (hxy : x ≤ y) : suzukiUpperSourcePairing suzukiStandardUpperAdjoint y = suzukiUpperSourcePairing suzukiStandardUpperAdjoint x

Production conservation theorem for the genuine upper source and genuine standard adjoint.

theorem MathlibNt.SieveTheory.tendsto_suzukiUpperSourcePairing_two (hP : SuzukiUpperSourcePTail) (hp : SuzukiStandardUpperAdjointScaledTail) (hwindow : SuzukiUpperSourcePairingWindowTail) : Filter.Tendsto (suzukiUpperSourcePairing suzukiStandardUpperAdjoint) Filter.atTop (nhds 2)

The upper pairing tends to 2 from the genuine source tail, the elementary scaled Laplace tail, and the residual unit-window estimate.

theorem MathlibNt.SieveTheory.suzukiUpperSourcePairing_eq_two (hDDE : SuzukiUpperSourcePIntegralDDE) (hpDDE : SuzukiStandardUpperAdjointDDE) (hPtail : SuzukiUpperSourcePTail) (hptail : SuzukiStandardUpperAdjointScaledTail) (hwindow : SuzukiUpperSourcePairingWindowTail) {s : ℝ} (hs : 2 ≤ s) : suzukiUpperSourcePairing suzukiStandardUpperAdjoint s = 2

No invocation of Proposition 11.8(iii): conservation transports the independently computed value at infinity back to every finite s ≥ 2.