Proposition 11.8 from finite full-layer prefixes

The prefix below follows the production source definition exactly. Above the source boundary it contains the first m odd and first m even source layers; below the boundary it uses the finite amplitude A_m / s. Thus the initial history is part of the prefix, rather than being silently replaced by the out-of-domain values of the recursive layer formula.

noncomputable def MathlibNt.SieveTheory.suzukiProposition118SourceQPrefix (m : ℕ) (s : ℝ) : ℝ

The genuine full source prefix, including its prescribed initial history.

Equations

• MathlibNt.SieveTheory.suzukiProposition118SourceQPrefix m s = if s < 2 then MathlibNt.SieveTheory.suzukiFiniteLowerAmplitude m / s else MathlibNt.SieveTheory.suzukiOddSourceUpperPartialSum m s + MathlibNt.SieveTheory.suzukiEvenSourceLowerPartialSum m s

noncomputable def MathlibNt.SieveTheory.suzukiProposition118SourceQTerminal (m : ℕ) (s : ℝ) : ℝ

Only the last even layer is left after the finite weighted source equations telescope. It starts at the true delayed source boundary s=3; below that point the finite initial history closes the telescope exactly.

Equations

• MathlibNt.SieveTheory.suzukiProposition118SourceQTerminal m s = if 3 < s then MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * m) (s - 1) else 0

noncomputable def MathlibNt.SieveTheory.suzukiProposition118SourceQTerminalPairingResidual (m : ℕ) (y : ℝ) : ℝ

The corresponding single-terminal-layer pairing residual.

Equations

• MathlibNt.SieveTheory.suzukiProposition118SourceQTerminalPairingResidual m y = ∫ (s : ℝ) in 2..y, MathlibNt.SieveTheory.suzukiProposition118KappaOneSourceAdjoint s * MathlibNt.SieveTheory.suzukiProposition118SourceQTerminal m s

theorem MathlibNt.SieveTheory.suzukiLayer_weighted_eq_integral_to_upper {β s : ℝ} {n : ℕ} (hβ : 1 < β) (hn : 2 ≤ n) (hs : β + ↑(SuzukiFiniteContinuousLayers.sourceEpsilon n) ≤ s) : s * SuzukiFiniteContinuousLayers.suzukiLayer 1 β n s = ∫ (t : ℝ) in s..β + ↑n, SuzukiFiniteContinuousLayers.suzukiLayer 1 β (n - 1) (t - 1)

theorem MathlibNt.SieveTheory.hasDerivAt_weighted_suzukiLayer_of_threshold_lt {β s : ℝ} {n : ℕ} (hβ : 1 < β) (hn : 2 ≤ n) (hs : β + ↑(SuzukiFiniteContinuousLayers.sourceEpsilon n) < s) : HasDerivAt (fun (u : ℝ) => u * SuzukiFiniteContinuousLayers.suzukiLayer 1 β n u) (-SuzukiFiniteContinuousLayers.suzukiLayer 1 β (n - 1) (s - 1)) s

Away from its parity threshold, the weighted recursive layer has the literal source derivative. No infinite sum is differentiated.