The finite lower-boundary constant and its real limit

This module records the unconditional consequences of the already proved real summability. It does not assume or define Suzuki's source normalization B=0.

noncomputable def MathlibNt.SieveTheory.suzukiLowerBoundaryLimit : ℝ

The real limiting lower-boundary constant at κ=1, β=2.

Equations

• MathlibNt.SieveTheory.suzukiLowerBoundaryLimit = 2 * (1 - MathlibNt.SieveTheory.suzukiEvenSourceLowerLayerLimit 2)

theorem MathlibNt.SieveTheory.antitone_suzukiFiniteLowerBoundary : Antitone suzukiFiniteLowerBoundary

The finite constants B_m=2(1-T_{2m}(2)) decrease with depth.

theorem MathlibNt.SieveTheory.suzuki_finite_lower_normalization (m : ℕ) : 2 * suzukiEvenSourceLowerPartialSum m 2 = 2 - suzukiFiniteLowerBoundary m

Exact finite normalization 2*T_{2m}(2)=2-B_m.

theorem MathlibNt.SieveTheory.tendsto_suzukiFiniteLowerBoundary {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : Filter.Tendsto suzukiFiniteLowerBoundary Filter.atTop (nhds suzukiLowerBoundaryLimit)

The finite boundary constants converge in ℝ to their genuine series normalization.

theorem MathlibNt.SieveTheory.suzukiLowerBoundaryLimit_eq_zero_iff : suzukiLowerBoundaryLimit = 0 ↔ suzukiEvenSourceLowerLayerLimit 2 = 1

Suzuki's B=0 is exactly normalization of the even lower mass to one.