def MathlibNt.SieveTheory.Proposition118InitialStripSourceBound : Prop

Proposition 11.8, specialized to the compact source strip needed in Suzuki (13.11).

Equations

• MathlibNt.SieveTheory.Proposition118InitialStripSourceBound = ∃ (B : ℝ), 0 ≤ B ∧ ∀ (N : ℕ) (x : ℝ), 1 ≤ N → x ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N → x ≤ 4 → x * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N x ≤ B

theorem MathlibNt.SieveTheory.proposition118_initialStrip_of_summable_layer_majorant (a : ℕ → ℝ) (ha0 : ∀ (n : ℕ), 0 ≤ a n) (ha : Summable a) (hmajor : ∀ (n : ℕ), ∀ x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 n, x ≤ 4 → x * SuzukiFiniteContinuousLayers.suzukiLayer 1 2 n x ≤ a n) : Proposition118InitialStripSourceBound

A summable depth majorant is the precise convergence input from which the uniform compact-strip consequence follows. This lemma contains no finite scan: the same sequence majorizes every legal compact-strip coordinate.