noncomputable def MathlibNt.SieveTheory.lemma144BaseOneUniformConstant (K Δ : ℝ) : ℝ

An explicit constant which absorbs the depth-one local-product remainder uniformly for every natural source coordinate D ≥ 2.

Equations

• MathlibNt.SieveTheory.lemma144BaseOneUniformConstant K Δ = 9 * K * Real.log 2 ^ (Δ - 1) / Real.exp √K

noncomputable def MathlibNt.SieveTheory.lemma144BaseOneGlobalConstant (Δ : ℝ) : ℝ

A depth-one constant independent of the dimension bound K.

Equations

• MathlibNt.SieveTheory.lemma144BaseOneGlobalConstant Δ = 18 * Real.log 2 ^ (Δ - 1)

theorem MathlibNt.SieveTheory.lemma144BaseOneUniformConstant_le_global {K Δ : ℝ} (hK : 0 ≤ K) : lemma144BaseOneUniformConstant K Δ ≤ lemma144BaseOneGlobalConstant Δ

theorem MathlibNt.SieveTheory.lemma14_4_base_one_odd_low_allD {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {d Δ C K : ℝ} (hΔ1 : Δ < 1) (hC : lemma144BaseOneUniformConstant K Δ ≤ C) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (D : ℕ) (s : ℝ) : 2 ≤ D → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 1 → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → ¬2 ≤ s → suzukiActualT S 1 D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 1 s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H 1 (↑D) d s * Real.log ↑D ^ (-Δ))

The genuine depth-one, odd low-strip base at every D ≥ 2. Unlike the previous eventual theorem, this has no Dmin and no abstract Case-II premise: the explicit K,Δ-uniform constant absorbs the local-product loss.

theorem MathlibNt.SieveTheory.lemma14_4_base_one_odd_low_allD_global {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {d Δ C K : ℝ} (hΔ1 : Δ < 1) (hC : lemma144BaseOneGlobalConstant Δ ≤ C) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (D : ℕ) (s : ℝ) : 2 ≤ D → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 1 → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → ¬2 ≤ s → suzukiActualT S 1 D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 1 s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H 1 (↑D) d s * Real.log ↑D ^ (-Δ))

K-uniform version of the odd low-strip base.

theorem MathlibNt.SieveTheory.lemma14_4_base_one_lowStrip_global_allD {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {d Δ C K : ℝ} (hΔ1 : Δ < 1) (hC : lemma144BaseOneGlobalConstant Δ ≤ C) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (D : ℕ) (s : ℝ) : 2 ≤ D → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 1 → s ≤ 3 → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → suzukiActualT S 1 D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 1 s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H 1 (↑D) d s * Real.log ↑D ^ (-Δ))

The complete depth-one estimate on the source low strip 1 < s ≤ 3, for all D ≥ 2, with a constant independent of K.