Real convergence of the even lower source layers

This module turns the all-depth source/hat comparison proved in the production Lemma 13.2 development into genuine real summability. In particular, the ENNReal supremum used by SuzukiFiniteSourceLayerEvenLimit is finite whenever the production Section-13 source contract is available. No finite scan and no caller-supplied summable sequence occurs here.

theorem MathlibNt.SieveTheory.suzukiEvenSourceLowerPartialSum_bounded_of_sourceContract {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs : 2 ≤ s) : ∃ (B : ℝ), ∀ (m : ℕ), suzukiEvenSourceLowerPartialSum m s ≤ B

The production all-depth comparison supplies a single bound for every even partial sum at a fixed lower-parity coordinate.

theorem MathlibNt.SieveTheory.summable_suzukiLayer_one_two_even_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

The actual even lower-layer sequence is summable; the majorization is produced by the production all-depth source/hat theorem, rather than accepted as an abstract Summable premise.

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

The finite real value of the even lower source-layer series.

Equations

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

theorem MathlibNt.SieveTheory.tendsto_suzukiEvenSourceLowerPartialSum_real {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs : 2 ≤ s) : Filter.Tendsto (fun (m : ℕ) => suzukiEvenSourceLowerPartialSum m s) Filter.atTop (nhds (suzukiEvenSourceLowerLayerLimit s))

Real partial sums converge to the genuine tsum.

theorem MathlibNt.SieveTheory.suzukiEvenSourceLowerLayerSup_eq_ofReal_limit {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs : 2 ≤ s) : suzukiEvenSourceLowerLayerSup s = ENNReal.ofReal (suzukiEvenSourceLowerLayerLimit s)

The unconditional extended supremum is the ofReal image of the real series value.

theorem MathlibNt.SieveTheory.suzukiEvenSourceLowerLayerSup_ne_top_of_sourceContract {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs : 2 ≤ s) : suzukiEvenSourceLowerLayerSup s ≠ ⊤

In particular the lower-layer supremum is finite.

theorem MathlibNt.SieveTheory.proposition118_initialStripSourceBound_of_sourceContract {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : Proposition118InitialStripSourceBound

Proposition 11.8's compact-strip consequence is produced from the same all-depth source comparison. Compactness is used only in the real coordinate; there is no scan over depths.