Convergence of Suzuki's finite lower amplitude

The same all-depth Lemma 13.2 source contract that bounds the even lower layers also bounds the odd source layers at s = 3. Hence their partial sums converge to the tsum occurring in Suzuki's canonical first-interval amplitude. This closes the A_m - A term in the finite residual decomposition.

theorem MathlibNt.SieveTheory.suzukiOddSourceUpperPartialSum_succ (m : ℕ) (s : ℝ) : suzukiOddSourceUpperPartialSum (m + 1) s = suzukiOddSourceUpperPartialSum m s + SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * m + 1) s

Adding one term to the odd source partial sum.

theorem MathlibNt.SieveTheory.finiteSourceLayer_two_mul_add_one_eq_oddPartialSum (m : ℕ) (s : ℝ) : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (2 * m + 1) s = suzukiOddSourceUpperPartialSum (m + 1) s

The odd source layer at depth 2m+1 is exactly the first m+1 odd continuous layers.

theorem MathlibNt.SieveTheory.suzukiOddSourceUpperPartialSum_bounded_of_sourceContract {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (B : ℝ), ∀ (m : ℕ), suzukiOddSourceUpperPartialSum m 3 ≤ B

Lemma 13.2 gives one real upper bound for all odd partial sums at the source endpoint s = 3.

theorem MathlibNt.SieveTheory.summable_suzukiLayer_one_two_odd_at_three_of_sourceContract {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : Summable fun (k : ℕ) => SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) 3

The actual odd source-layer sequence at s = 3 is summable, with no caller-supplied majorant.

theorem MathlibNt.SieveTheory.tendsto_suzukiOddSourceUpperPartialSum {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : Filter.Tendsto (fun (m : ℕ) => suzukiOddSourceUpperPartialSum m 3) Filter.atTop (nhds (∑' (k : ℕ), SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) 3))

Odd finite partial sums converge to the exact tsum used in the canonical amplitude.

theorem MathlibNt.SieveTheory.tendsto_suzukiFiniteLowerAmplitude {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : Filter.Tendsto suzukiFiniteLowerAmplitude Filter.atTop (nhds SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude)

The finite first-interval amplitudes A_m converge to Suzuki's canonical amplitude A.

theorem MathlibNt.SieveTheory.tendsto_suzukiFiniteLowerAmplitude_residual_zero {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (s : ℝ) : Filter.Tendsto (fun (m : ℕ) => (suzukiFiniteLowerAmplitude m - SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude) / s * ∫ (t : ℝ) in 2..s, (t - 1)⁻¹) Filter.atTop (nhds 0)

The A_m-A contribution in the first-interval residual decomposition tends to zero (for every fixed real coordinate s).