theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.suzukiVProduct_div_eq_suffix
(S : BoundingSieve)
{p : ℕ}
{z : ℝ}
(hpz : ↑p < z)
:
suzukiVProduct S ↑p / suzukiVProduct S z = ∏ q ∈ S.prodPrimes.primeFactors with p ≤ q ∧ ↑q < z, (1 - S.nu q)⁻¹
The concrete Euler-product quotient occurring in sigmaTwelve is exactly
its Lemma-8.7 suffix product.
theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.naturalCeil_inherited_error_le_claim14_13
(H : Section13HatLayers)
{N D p : ℕ}
{d Δ : ℝ}
(hp : 2 ≤ p)
(hDp : 2 * p ≤ D)
(hΔ : 0 ≤ Δ)
(hT : 0 ≤ H.T (ErrorSign.ofDepth (N - 1)) (SuzukiLemma144Equation1410.inheritedCoordinate D p))
(h1413 : Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p))
:
Source-coordinate version of the natural-ceiling error estimate. Unlike
naturalCeil_error_le_claim14_13, this is the form needed by the literal
equation14_10.sigmaTwelve, whose envelope is evaluated at the inherited
coordinate.
theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigmaTwelve_suzukiVProduct_le_qD_lemma8_7
{S : BoundingSieve}
{H : Section13HatLayers}
{β C K d Δ w v s τ σ : ℝ}
{N D znat : ℕ}
(hH : Section13HatContract H β)
(hD : 1 < ↑D)
(hz2 : 2 ≤ ↑znat)
(hv2 : 2 ≤ v)
(hw2 : 2 ≤ w)
(hwv : w ≤ v)
(hvz : v ≤ ↑znat)
(hz : ↑znat = ↑D ^ (1 / s))
(hv : v = ↑D ^ (1 / τ))
(hw : w = ↑D ^ (1 / σ))
(hτ : H.betaHat + (ErrorSign.ofDepth N).epsilon < τ)
(hτσ : τ ≤ σ)
(hK : 2 ≤ K)
(hlocal : HasDimensionOneLocalProductBound S K)
(hii : 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 (ErrorSign.ofDepth (N - 1)) (SuzukiLemma144Equation1410.inheritedCoordinate D p))
(h1413 :
∀ p ∈ S.prodPrimes.primeFactors,
w ≤ ↑p → ↑p < v → Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p))
:
SuzukiLemma144Equation1410.sigmaTwelve S.prodPrimes.primeFactors (⇑S.nu) (fun (p : ℕ) => suzukiVProduct S ↑p)
(fun (n D' : ℕ) (x : ℝ) => errorEnvelope H n (↑D') d x) (suzukiVProduct S ↑znat) C K Δ N D σ τ ≤ C * Real.exp √K * suzukiVProduct S ↑znat * (Real.log ↑D ^ (-Δ) * ((1 / s * ∫ (t : ℝ) in τ..σ, qD H (ErrorSign.ofDepth N).opposite (↑D) d Δ t) + 6 * K ^ 2 * qD H (ErrorSign.ofDepth N).opposite (↑D) d Δ τ / Real.log w * (τ / s)))
Global scaling closure of the concrete sigmaTwelve from (14.10), followed
by the exact integral-plus-endpoint conclusion of qD Lemma 8.7.