Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiFiniteLowerBoundaryLimit

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.

source
noncomputable def MathlibNt.SieveTheory.suzukiLowerBoundaryLimit :
ℝ

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

Equations
Instances For
    source
    theorem MathlibNt.SieveTheory.antitone_suzukiFiniteLowerBoundary :
    Antitone suzukiFiniteLowerBoundary

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

    source
    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.

    source
    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.

    source
    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.