theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qDClamp_conditions_of_claim14_6_ii_closed
{H : Section13HatLayers}
{β D d Δ τ σ : ℝ}
(hH : Section13HatContract H β)
(sign : ErrorSign)
(hD : 1 < D)
(hτ : H.betaHat + sign.epsilon ≤ τ)
(_hτσ : τ ≤ σ)
(hii : Claim14_6_MonotoneQPremise H D d Δ σ)
:
Closed-endpoint form of the qD clamp conditions. The only extra case
relative to the legacy strict theorem is the lower endpoint itself; continuity
extends weighted antitonicity from Ioc to that endpoint.
theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma8_7_qD_of_claim14_6_ii_closed
{S : BoundingSieve}
{H : Section13HatLayers}
{β D z v w s τ σ K d Δ : ℝ}
(sign : ErrorSign)
(hH : Section13HatContract H β)
(hD : 1 < D)
(hz2 : 2 ≤ z)
(hv2 : 2 ≤ v)
(hw2 : 2 ≤ w)
(hwv : w ≤ v)
(hvz : v ≤ z)
(hz : z = D ^ (1 / s))
(hv : v = D ^ (1 / τ))
(hw : w = D ^ (1 / σ))
(hτ : H.betaHat + sign.epsilon ≤ τ)
(hτσ : τ ≤ σ)
(hK : 2 ≤ K)
(hlocal : HasDimensionOneLocalProductBound S K)
(hii : Claim14_6_MonotoneQPremise H D d Δ σ)
:
Lemma 8.7 for qD at the source-faithful closed lower endpoint.
theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigma12_middle_le_qD_lemma8_7_closed
{S : BoundingSieve}
{H : Section13HatLayers}
{β D z v w s τ σ K d Δ : ℝ}
(sign : ErrorSign)
(R : ℝ → ℝ)
(hmajorant :
∀ p ∈ S.prodPrimes.primeFactors,
w ≤ ↑p → ↑p < v → R (Real.log D / Real.log ↑p) ≤ qD H sign.opposite D d Δ (Real.log D / Real.log ↑p))
(hH : Section13HatContract H β)
(hD : 1 < D)
(hz2 : 2 ≤ z)
(hv2 : 2 ≤ v)
(hw2 : 2 ≤ w)
(hwv : w ≤ v)
(hvz : v ≤ z)
(hz : z = D ^ (1 / s))
(hv : v = D ^ (1 / τ))
(hw : w = D ^ (1 / σ))
(hτ : H.betaHat + sign.epsilon ≤ τ)
(hτσ : τ ≤ σ)
(hK : 2 ≤ K)
(hlocal : HasDimensionOneLocalProductBound S K)
(hii : Claim14_6_MonotoneQPremise H D d Δ σ)
:
Closed-endpoint Σ₁₂ middle-range assembly.
theorem
MathlibNt.SieveTheory.sigmaTwelve_suzukiVProduct_le_qD_lemma8_7_natCeil_closed
{S : BoundingSieve}
{H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers}
{β C K d Δ w v s τ σ : ℝ}
{N D znat : ℕ}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H β)
(hD : 1 < ↑D)
(hv2 : 2 ≤ v)
(hw2 : 2 ≤ w)
(hwv : w ≤ v)
(hvz : v ≤ ↑D ^ (1 / s))
(hz : znat = ⌈↑D ^ (1 / s)⌉₊)
(hv : v = ↑D ^ (1 / τ))
(hw : w = ↑D ^ (1 / σ))
(hτ : H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ τ)
(hτσ : τ ≤ σ)
(hK : 2 ≤ K)
(hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K)
(hii : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneQPremise H (↑D) d Δ σ)
(hC : 0 ≤ C)
(hΔ : 0 ≤ Δ)
(hCeil : ∀ p ∈ S.prodPrimes.primeFactors, w ≤ ↑p → ↑p < v → 2 ≤ p ∧ 2 * p ≤ D)
(hT :
∀ p ∈ S.prodPrimes.primeFactors,
w ≤ ↑p →
↑p < v →
0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1))
(SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p))
(h1413 :
∀ p ∈ S.prodPrimes.primeFactors,
w ≤ ↑p →
↑p < v →
SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p)
(↑D / ↑p))
:
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve S.prodPrimes.primeFactors (⇑S.nu)
(fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p)
(fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x)
(SwitchingPrinciple.suzukiVProduct S ↑znat) C K Δ N D σ τ ≤ C * Real.exp √K * SwitchingPrinciple.suzukiVProduct S ↑znat * (Real.log ↑D ^ (-Δ) * ((1 / s * ∫ (t : ℝ) in τ..σ, SwitchingPrinciple.SuzukiLemma144KappaOne.qD H
(SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ t) + 6 * K ^ 2 * SwitchingPrinciple.SuzukiLemma144KappaOne.qD H
(SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ τ / Real.log w * (τ / s)))
Natural-ceiling Σ₁₂ estimate at the closed lower endpoint.