Suzuki Proposition 11.8: source parity series and the boundary pairing

This module uses the actual source layers fₙ of (9.1)--(9.2), not the Section-13 hat solutions. At κ = 1, β = 2, equation (9.5) is

• T⁺(s) = ∑' k, f_{2k+1}(s) on s > 1;
• T⁻(s) = ∑' k, f_{2(k+1)}(s) on s ≥ 2.

As on printed pp. 63--65, Proposition 11.8 extends P = T⁺ - T⁻ + 2 and Q = T⁺ + T⁻ from s ≥ β to the initial interval by s P(s) = s Q(s) = A. We then evaluate the genuine Section-10 Iwaniec pairing of this source Q with q(s)=s-1 at β=2.

noncomputable def MathlibNt.SieveTheory.suzukiProposition118SourceTPlus (s : ℝ) : ℝ

Suzuki (9.5), positive/odd parity source series T⁺.

Equations

• MathlibNt.SieveTheory.suzukiProposition118SourceTPlus s = ∑' (k : ℕ), MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) s

noncomputable def MathlibNt.SieveTheory.suzukiProposition118SourceTMinus (s : ℝ) : ℝ

Suzuki (9.5), negative/even parity source series T⁻.

Equations

• MathlibNt.SieveTheory.suzukiProposition118SourceTMinus s = ∑' (k : ℕ), MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1)) s

@[simp]

theorem MathlibNt.SieveTheory.suzukiProposition118SourceTMinus_eq (s : ℝ) : suzukiProposition118SourceTMinus s = suzukiEvenSourceLowerLayerLimit s

theorem MathlibNt.SieveTheory.suzukiLayer_one_two_odd_nonneg {s : ℝ} (hs : 1 < s) (k : ℕ) : 0 ≤ SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) s

Every odd source layer is nonnegative on its exact source domain s > 1.

theorem MathlibNt.SieveTheory.suzukiOddSourceUpperPartialSum_bounded_of_sourceContract_at {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs : 1 < s) : ∃ (B : ℝ), ∀ (m : ℕ), suzukiOddSourceUpperPartialSum m s ≤ B

The production all-depth comparison gives one bound for all odd source partial sums at every fixed point of the exact odd domain.

theorem MathlibNt.SieveTheory.summable_suzukiProposition118SourceTPlus_of_sourceContract {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs : 1 < s) : Summable fun (k : ℕ) => SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) s

Real summability of the actual odd source series throughout I⁺=(1,∞).

theorem MathlibNt.SieveTheory.summable_suzukiProposition118SourceTMinus_of_sourceContract {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs : 2 ≤ s) : Summable fun (k : ℕ) => SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1)) s

Real summability of the actual even source series throughout I⁻=[2,∞).

theorem MathlibNt.SieveTheory.mul_suzukiProposition118SourceTPlus_eq_amplitude_sub {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs1 : 1 < s) (hs3 : s ≤ 3) : s * suzukiProposition118SourceTPlus s = SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude - s

Proposition 9.4(vii), obtained as the real limit of the finite Proposition-9.3 identity, on the closed part of the first odd strip.

noncomputable def MathlibNt.SieveTheory.suzukiProposition118SourceQ (s : ℝ) : ℝ

The genuine source Q of Proposition 11.8. Below β=2 this is precisely its source-prescribed initial history, not a Section-13 hat function.

Equations

• MathlibNt.SieveTheory.suzukiProposition118SourceQ s = if s < 2 then MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude / s else MathlibNt.SieveTheory.suzukiProposition118SourceTPlus s + MathlibNt.SieveTheory.suzukiProposition118SourceTMinus s

noncomputable def MathlibNt.SieveTheory.suzukiProposition118SourceP (s : ℝ) : ℝ

The genuine source P of Proposition 11.8.

Equations

• MathlibNt.SieveTheory.suzukiProposition118SourceP s = if s < 2 then MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude / s else MathlibNt.SieveTheory.suzukiProposition118SourceTPlus s - MathlibNt.SieveTheory.suzukiProposition118SourceTMinus s + 2

theorem MathlibNt.SieveTheory.suzukiProposition118SourceQ_initial {s : ℝ} (hs1 : 1 < s) (hs2 : s < 2) : s * suzukiProposition118SourceQ s = SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude

The exact initial-history equation s Q(s)=A, printed before and in the proof of Proposition 11.8.

theorem MathlibNt.SieveTheory.suzukiProposition118SourceP_initial {s : ℝ} (hs1 : 1 < s) (hs2 : s < 2) : s * suzukiProposition118SourceP s = SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude

The exact initial-history equation s P(s)=A.

theorem MathlibNt.SieveTheory.suzukiProposition118SourceQ_at_two {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : suzukiProposition118SourceQ 2 = (SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude - suzukiLowerBoundaryLimit) / 2

At β=2, the source series has the boundary value Q(2)=(A-B)/2, deduced from the actual odd/even real series.

noncomputable def MathlibNt.SieveTheory.suzukiProposition118SourceQPairing (s : ℝ) : ℝ

The source Iwaniec pairing ⟨Q,q⟩ from Section 10, with b=κ=1.

Equations

• MathlibNt.SieveTheory.suzukiProposition118SourceQPairing s = MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10SignedPairing 1 MathlibNt.SieveTheory.suzukiProposition118SourceQ MathlibNt.SieveTheory.suzukiProposition118KappaOneSourceAdjoint s

theorem MathlibNt.SieveTheory.suzukiProposition118SourceQ_initialWindowIntegral : ∫ (t : ℝ) in 1..2, suzukiProposition118KappaOneSourceAdjoint (t + 1) * suzukiProposition118SourceQ t = SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude

On the initial pairing window [1,2], the integral term is exactly A. The exceptional boundary point t=2, where source Q switches from its initial history to the convergent parity series, is null for integration.

theorem MathlibNt.SieveTheory.suzukiProposition118SourceQPairing_at_lowerBoundary {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : suzukiProposition118SourceQPairing 2 = suzukiProposition118LowerBoundaryPairingScalar SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude

Proposition 11.8(iii)'s boundary evaluation for the genuine source series: ⟨Q,q⟩(β) is exactly the previously frozen scalar -B + A q(β-1). There is no pairing-zero or conclusion-shaped premise.