noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSevenPrimeSum (S : BoundingSieve) (D w v z : ℝ) (H : ℝ → ℝ) : ℝ

The middle-range prime sum in Suzuki Lemma 8.7 (dimension one): the prime range stops at v, while the Euler suffix ratio still stops at z.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSevenPrimeSum S D w v z H = ∑ p ∈ S.prodPrimes.primeFactors with w ≤ ↑p ∧ ↑p < v, (S.nu p * ∏ q ∈ S.prodPrimes.primeFactors with p ≤ q ∧ ↑q < z, (1 - S.nu q)⁻¹) * H (Real.log D / Real.log ↑p)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSevenPrimeSum_eq_localRatio_mul (S : BoundingSieve) (D w v z : ℝ) (H : ℝ → ℝ) (hvz : v ≤ z) : suzukiLemmaEightSevenPrimeSum S D w v z H = suzukiLocalRatio S v z * suzukiLemmaEightSixPrimeSum S D w v H

Exact factorization used in Suzuki's proof of Lemma 8.7.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSevenDimensionOne {S : BoundingSieve} {D z v w s τ σ K : ℝ} {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 / σ)) (hHcont : Continuous H) (hH0 : ∀ t ∈ Set.Icc τ σ, 0 ≤ H t) (hHt : AntitoneOn (fun (t : ℝ) => H t * t) (Set.Icc τ σ)) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) : suzukiLemmaEightSevenPrimeSum S D w v z H ≤ (1 / s * ∫ (t : ℝ) in τ..σ, H t) + 6 * K ^ 2 * H τ / Real.log w * (τ / s)

Suzuki Lemma 8.7, specialized to sieve dimension one (κ = 1). The sum is over the middle range w ≤ p < v, but retains the suffix ratio V(p)/V(z). The error is exactly 6 K² H(τ) / log w * (τ/s).