def MathlibNt.SieveTheory.Claim145CaseALowSSourceSigmaPrefactor (d Δ C1 Θ C : ℝ) : Prop

The strengthened prefactor estimate needed in the low-coordinate branch. Unlike the preliminary version, this statement retains the moving sourceSigma factor occurring in the denominator of Claim 14.5.

Equations

• MathlibNt.SieveTheory.Claim145CaseALowSSourceSigmaPrefactor d Δ C1 Θ C = ∀ᶠ (K : ℝ) in Filter.atTop, 2 ≤ K ∧ ∀ (D s : ℝ), 2 ≤ D → 2 ≤ s → s ≤ √K / Real.log K → Real.log D ≤ C1 * K ^ Θ → Real.log D / Real.log 2 * (1 + K / Real.log 2) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d * Real.log D ^ (1 + Δ) * Real.exp (C * s) ≤ Real.exp (√K / 2)

theorem MathlibNt.SieveTheory.proposition131iiUniformQuantitativeLower_from_two {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (sign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (s : ℝ), 2 ≤ s → SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C s ≤ H.T sign s

Proposition 13.1(ii)'s eventual lower profile can be enlarged in its linear loss so that it starts at s = 2. This is the compact initial interval which must be closed before the final low-s branch is genuinely uniform in s.

theorem MathlibNt.SieveTheory.one_le_claim145_local_factor_mul_vProduct (S : BoundingSieve) {D : ℕ} {K : ℝ} (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hD : 2 ≤ D) : 1 ≤ Real.log ↑D / Real.log 2 * (1 + K / Real.log 2) * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S ↑D

At the bottom endpoint 2, the local-product contract gives exactly the reciprocal Euler-product factor used by the prefactor estimate.

theorem MathlibNt.SieveTheory.claim145_caseA_lowS_target_le_equation14_6_lower (S : BoundingSieve) {D : ℕ} {d Δ K s C : ℝ} (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hD : 2 ≤ D) (hs : 2 ≤ s) (hpref : Real.log ↑D / Real.log 2 * (1 + K / Real.log 2) * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d * Real.log ↑D ^ (1 + Δ) * Real.exp (C * s) ≤ Real.exp (√K / 2)) : Real.exp (-s * Real.log s - s * Real.log (Real.log (3 * s)) + √K / 2) ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S ↑D * (Real.exp √K / (Real.log ↑D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)) * ((1 + s ^ d / Real.log ↑D) ^ s * s * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C s) * Real.log ↑D ^ (-Δ)

Pure terminal algebra: the sourceSigma-inclusive prefactor turns the second exponential comparison into the explicit lower side of (14.6).

theorem MathlibNt.SieveTheory.claim145_caseA_lowS_actual_of_bigOScalarTarget (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hbigO : Claim145CaseALowSBigOScalarTarget C1 Θ) (hpref : ∀ (C : ℝ), 0 ≤ C → Claim145CaseALowSSourceSigmaPrefactor d Δ C1 Θ C) : ∃ (K0 : ℝ), 2 ≤ K0 ∧ Claim145CaseALargeKLowSClosed S H d Δ C1 Θ K0 1

Final Case-A low-s assembly. A single K0 is selected before K,N,D,s; the conclusion is the actual production Claim14_5Bound (through its source-native spelling ActualClaim145BoundAt), with constant one.

theorem MathlibNt.SieveTheory.claim145_caseA_lowS_actual (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC1 : 0 ≤ C1) (hΘ : 0 < Θ) (hd : 0 < d) (hsource : 2 / d < 1 / Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) : ∃ (K0 : ℝ), 2 ≤ K0 ∧ Claim145CaseALargeKLowSClosed S H d Δ C1 Θ K0 1

Closed production-facing low-s leaf, using the strengthened sourceSigma-inclusive prefactor theorem. The first source big-O estimate is supplied by claim145_caseA_lowS_bigOScalarTarget.

theorem MathlibNt.SieveTheory.claim145_caseA_lowS_actual_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC1 : 0 ≤ C1) (hΘ : 0 < Θ) (hd : 0 < d) (hsource : 2 / d < 1 / Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) : ∃ (K0 : ℝ), 2 ≤ K0 ∧ ∀ (S : BoundingSieve), Claim145CaseALargeKLowSClosed S H d Δ C1 Θ K0 1

Uniform-in-sieve strengthening of the low-coordinate Case-A leaf. All analytic witnesses and the K threshold are chosen before the varying sieve.