Dimension-one prime sums and finite Abel identities

Local product bounds, finite prime nodes, and Abel summation establish the dimension-one prime-sum comparison of Suzuki's Lemma 8.6.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

def MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound (S : BoundingSieve) (K : ℝ) : Prop

The standard dimension-one local-product condition V(z₁)/V(z₂) ≤ (log z₂/log z₁)(1 + K/log z₁). The product is restricted to the actual finite sieving primes, so omitted Goldbach primes dividing N are handled without changing the abstract hypothesis.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound S K = ∀ (z₁ z₂ : ℝ), 2 ≤ z₁ → z₁ ≤ z₂ → ∏ p ∈ S.prodPrimes.primeFactors with z₁ ≤ ↑p ∧ ↑p < z₂, (1 - S.nu p)⁻¹ ≤ Real.log z₂ / Real.log z₁ * (1 + K / Real.log z₁)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLocalRatio (S : BoundingSieve) (w z : ℝ) : ℝ

The finite-support version of Suzuki's ratio V(w) / V(z), restricted to the actual sieving primes.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLocalRatio S w z = ∏ p ∈ S.prodPrimes.primeFactors with w ≤ ↑p ∧ ↑p < z, (1 - S.nu p)⁻¹

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzuki_supportedPrimes_real_eq_inter_Ico (S : BoundingSieve) {w z : ℝ} (_hw : 0 ≤ w) (_hz : 0 ≤ z) : {p ∈ S.prodPrimes.primeFactors | w ≤ ↑p ∧ ↑p < z} = S.prodPrimes.primeFactors ∩ Finset.Ico ⌈w⌉₊ ⌈z⌉₊

For nonnegative real cutoffs, the supported primes in [w,z) are exactly those in the natural half-open interval [⌈w⌉₊,⌈z⌉₊).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzuki_supportedPrimes_real_eq_ceil (S : BoundingSieve) {w z : ℝ} (hw : 0 ≤ w) (hz : 0 ≤ z) : {p ∈ S.prodPrimes.primeFactors | w ≤ ↑p ∧ ↑p < z} = {p ∈ S.prodPrimes.primeFactors | ⌈w⌉₊ ≤ p ∧ p < ⌈z⌉₊}

Filter-form corollary of the exact real/natural carrier bridge.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiDimensionOneError (S : BoundingSieve) (w z : ℝ) : ℝ

Suzuki's dimension-one local-product error E(w,z).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiDimensionOneError S w z = MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLocalRatio S w z - Real.log z / Real.log w

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiDimensionOneError_le {S : BoundingSieve} {K w z : ℝ} (hlocal : HasDimensionOneLocalProductBound S K) (hw : 2 ≤ w) (hwz : w ≤ z) : suzukiDimensionOneError S w z ≤ K / Real.log w * (Real.log z / Real.log w)

Suzuki equation (8.1) in dimension one follows directly from the generic local-product condition; no prime-specific PNT or Mertens theorem is used.

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

The exact finite prime sum on the left side of Suzuki Lemma 8.6 in sieve dimension one. The suffix product is the finite ratio V(p)/V(z).

Equations

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

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow (S : BoundingSieve) (z : ℕ) : Finset ℕ

Supported primes below the natural cutoff z.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z = {q ∈ S.prodPrimes.primeFactors | q < z}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSuffixRatio (S : BoundingSieve) (z n : ℕ) : ℝ

The finite suffix Euler ratio over supported primes n ≤ q < z.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSuffixRatio S z n = ∏ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z with n ≤ q, (1 - S.nu q)⁻¹

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLocalRatio_eq_suzukiSuffixRatio_ceil (S : BoundingSieve) {w z : ℝ} (hw : 0 ≤ w) (hz : 0 ≤ z) : suzukiLocalRatio S w z = suzukiSuffixRatio S ⌈z⌉₊ ⌈w⌉₊

Exact bridge from real cutoffs to natural ceiling cutoffs. In particular, an integral right endpoint retains the strict condition p < z.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLocalRatio_nat_right (S : BoundingSieve) {w : ℝ} (z : ℕ) (hw : 0 ≤ w) : suzukiLocalRatio S w ↑z = suzukiSuffixRatio S z ⌈w⌉₊

At a natural right endpoint the ceiling bridge has no off-by-one shift.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSuffixRatio_step_of_mem (S : BoundingSieve) (z n : ℕ) (hn : n ∈ suzukiSupportedBelow S z) : suzukiSuffixRatio S z n = (1 - S.nu n)⁻¹ * suzukiSuffixRatio S z (n + 1)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSuffixRatio_step_of_not_mem (S : BoundingSieve) (z n : ℕ) (hn : n ∉ suzukiSupportedBelow S z) : suzukiSuffixRatio S z n = suzukiSuffixRatio S z (n + 1)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSuffixRatio_sub_succ (S : BoundingSieve) (z n : ℕ) : suzukiSuffixRatio S z n - suzukiSuffixRatio S z (n + 1) = if n ∈ suzukiSupportedBelow S z then S.nu n * suzukiSuffixRatio S z n else 0

Exact difference of consecutive finite suffix Euler products. The factor is R n, not R (n+1).

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiPrimeSumNat (S : BoundingSieve) (w z : ℕ) (F : ℕ → ℝ) : ℝ

Natural-cutoff version of Suzuki's finite prime sum.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiPrimeSumNat S w z F = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z with w ≤ p, S.nu p * MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSuffixRatio S z p * F p

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiPrimeSumNat_eq_abelSum (S : BoundingSieve) (w z : ℕ) (F : ℕ → ℝ) : suzukiPrimeSumNat S w z F = ∑ n ∈ Finset.Ico w z, (suzukiSuffixRatio S z n - suzukiSuffixRatio S z (n + 1)) * F n

The Suzuki prime sum is exactly the finite Abel difference sum; unsupported indices contribute zero by the suffix-product difference identity.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.finiteAbelIdentity (R F : ℕ → ℝ) (w z : ℕ) (hwz : w ≤ z) : ∑ n ∈ Finset.Ico w z, (R n - R (n + 1)) * F n = R w * F w - R z * F z + ∑ n ∈ Finset.Ico (w + 1) (z + 1), R n * (F n - F (n - 1))

Finite Abel (summation-by-parts) identity on a natural interval. This boundary convention remains valid for the empty interval w = z.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiPrimeSumNat_abelIdentity (S : BoundingSieve) (w z : ℕ) (hwz : w ≤ z) (F : ℕ → ℝ) : suzukiPrimeSumNat S w z F = suzukiSuffixRatio S z w * F w - suzukiSuffixRatio S z z * F z + ∑ n ∈ Finset.Ico (w + 1) (z + 1), suzukiSuffixRatio S z n * (F n - F (n - 1))

Suzuki's supported-prime sum in Abel boundary-plus-increment form.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSixPrimeSum_eq_nat (S : BoundingSieve) (D : ℝ) (w z : ℕ) (H : ℝ → ℝ) : suzukiLemmaEightSixPrimeSum S D (↑w) (↑z) H = suzukiPrimeSumNat S w z fun (p : ℕ) => H (Real.log D / Real.log ↑p)

At integral cutoffs, the current Suzuki prime-sum interface is exactly the natural supported-prime sum used by the finite Abel identity.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSixPrimeSum_abelIdentity (S : BoundingSieve) (D : ℝ) (w z : ℕ) (hwz : w ≤ z) (H : ℝ → ℝ) : suzukiLemmaEightSixPrimeSum S D (↑w) (↑z) H = suzukiSuffixRatio S z w * H (Real.log D / Real.log ↑w) - suzukiSuffixRatio S z z * H (Real.log D / Real.log ↑z) + ∑ n ∈ Finset.Ico (w + 1) (z + 1), suzukiSuffixRatio S z n * (H (Real.log D / Real.log ↑n) - H (Real.log D / Real.log ↑(n - 1)))

Thus the exact Suzuki prime sum at integral cutoffs has the Abel boundary-plus-increment expansion.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSuffixRatio_le {S : BoundingSieve} {K : ℝ} (hlocal : HasDimensionOneLocalProductBound S K) {x z : ℕ} (hx : 2 ≤ x) (hxz : x ≤ z) : suzukiSuffixRatio S z x ≤ Real.log ↑z / Real.log ↑x * (1 + K / Real.log ↑x)

The generic local-product input specializes exactly to the natural suffix ratio used by suzukiFiniteAbel.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiNatDimensionOneError_le {S : BoundingSieve} {K : ℝ} (hlocal : HasDimensionOneLocalProductBound S K) {x z : ℕ} (hx : 2 ≤ x) (hxz : x ≤ z) : suzukiSuffixRatio S z x - Real.log ↑z / Real.log ↑x ≤ K / Real.log ↑x * (Real.log ↑z / Real.log ↑x)

Equation (8.1) at natural endpoints, obtained without PNT or Mertens.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.antitoneOn_of_mul_id_antitoneOn {H : ℝ → ℝ} {s σ : ℝ} (hs : 0 < s) (hH0 : ∀ t ∈ Set.Icc s σ, 0 ≤ H t) (hmono : AntitoneOn (fun (t : ℝ) => H t * t) (Set.Icc s σ)) : AntitoneOn H (Set.Icc s σ)

The source hypothesis that t ↦ H(t)t is antitone, together with nonnegativity and positive coordinates, implies that H itself is antitone.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedPrimeNodes (S : BoundingSieve) (w z : ℝ) : List ℝ

The supported primes in [w,z), sorted and cast to real nodes.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedPrimeNodes S w z = List.map (fun (p : ℕ) => ↑p) ({p ∈ S.prodPrimes.primeFactors | w ≤ ↑p ∧ ↑p < z}.sort fun (x1 x2 : ℕ) => x1 ≤ x2)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodes (S : BoundingSieve) (w z : ℝ) : List ℝ

The complete real node list: the genuine lower endpoint, all supported prime jumps, and the genuine upper endpoint.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodes S w z = w :: MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedPrimeNodes S w z ++ [z]

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAtom (S : BoundingSieve) (z x y : ℝ) : ℝ

The local prime/jump atom attached to two consecutive real nodes.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAtom S z x y = MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLocalRatio S x z - MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLocalRatio S y z

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFinitePrimeAtom (S : BoundingSieve) (z : ℝ) (p : ℕ) : ℝ

Suzuki's source prime atom ω(p) V(p) / V(z).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFinitePrimeAtom S z p = S.nu p * MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLocalRatio S (↑p) z

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAtom_eq_primeAtom (S : BoundingSieve) (z y : ℝ) (p : ℕ) (hp : p ∈ S.prodPrimes.primeFactors) (hpz : ↑p < z) (hpy : ↑p < y) (hgap : ∀ q ∈ S.prodPrimes.primeFactors, p < q → ↑q < y → False) : suzukiFiniteNodeAtom S z (↑p) y = suzukiFinitePrimeAtom S z p

If y is the node immediately after a supported prime p, the successive node atom is exactly Suzuki's source prime atom. The hypotheses only express that no supported prime lies strictly between these two nodes.

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLocalRatio_self (S : BoundingSieve) (z : ℝ) : suzukiLocalRatio S z z = 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAbel (S : BoundingSieve) (w z : ℝ) (g : ℝ → ℝ) : LinearSieve.finiteNodeAtomSum (fun (x : ℝ) => suzukiLocalRatio S x z) g (suzukiFiniteNodes S w z) = suzukiLocalRatio S w z * g w - g z + LinearSieve.finiteNodeVariationSum (fun (x : ℝ) => suzukiLocalRatio S x z) g (suzukiFiniteNodes S w z)

Suzuki finite-node Abel summation. Unlike a natural-interval version, its boundary terms are exactly g w and g z. The summands on the left are the successive local-ratio (prime-jump) atoms.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAtomSum (S : BoundingSieve) (z : ℝ) (g : ℝ → ℝ) : List ℝ → ℝ

The Suzuki node-atom sum over consecutive pairs of a list.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAtomSum S z g (x_1 :: y :: xs) = MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAtom S z x_1 y * g x_1 + MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAtomSum S z g (y :: xs)
• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAtomSum S z g x✝ = 0

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAtomSum_eq (S : BoundingSieve) (z : ℝ) (g : ℝ → ℝ) (nodes : List ℝ) : suzukiFiniteNodeAtomSum S z g nodes = LinearSieve.finiteNodeAtomSum (fun (x : ℝ) => suzukiLocalRatio S x z) g nodes

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAbel_atoms (S : BoundingSieve) (w z : ℝ) (g : ℝ → ℝ) : suzukiFiniteNodeAtomSum S z g (suzukiFiniteNodes S w z) = suzukiLocalRatio S w z * g w - g z + LinearSieve.finiteNodeVariationSum (fun (x : ℝ) => suzukiLocalRatio S x z) g (suzukiFiniteNodes S w z)

The same specialization with the left side visibly written using Suzuki's successive local-ratio atoms.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAtomSum_eq_lemmaEightSixPrimeSum (S : BoundingSieve) (D w z : ℝ) (H : ℝ → ℝ) (_hwz : w ≤ z) : suzukiFiniteNodeAtomSum S z (fun (x : ℝ) => H (Real.log D / Real.log x)) (suzukiFiniteNodes S w z) = suzukiLemmaEightSixPrimeSum S D w z H

The real finite-node atom sum, with genuine endpoints w,z, is exactly Suzuki's finite prime sum for g x = H (log D / log x).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.transformedH_monotoneOn {D w z s σ : ℝ} {H : ℝ → ℝ} (hD : 1 < D) (hw : 1 < w) (_hwz : w ≤ z) (hcoord : ∀ x ∈ Set.Icc w z, Real.log D / Real.log x ∈ Set.Icc s σ) (hH : ∀ t ∈ Set.Icc s σ, 0 ≤ H t) (hHt : AntitoneOn (fun (t : ℝ) => H t * t) (Set.Icc s σ)) : MonotoneOn (fun (x : ℝ) => H (Real.log D / Real.log x)) (Set.Icc w z)

The Suzuki transform is increasing in the underlying variable.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedPrimeNodes_pairwise (S : BoundingSieve) (w z : ℝ) : List.Pairwise (fun (x1 x2 : ℝ) => x1 ≤ x2) (suzukiSupportedPrimeNodes S w z)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mem_suzukiSupportedPrimeNodes {S : BoundingSieve} {w z x : ℝ} (hx : x ∈ suzukiSupportedPrimeNodes S w z) : w ≤ x ∧ x < z

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodes_pairwise (S : BoundingSieve) {w z : ℝ} (hwz : w ≤ z) : List.Pairwise (fun (x1 x2 : ℝ) => x1 ≤ x2) (suzukiFiniteNodes S w z)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mem_suzukiFiniteNodes_Icc {S : BoundingSieve} {w z x : ℝ} (hwz : w ≤ z) (hx : x ∈ suzukiFiniteNodes S w z) : x ∈ Set.Icc w z

theorem MathlibNt.SieveTheory.SwitchingPrinciple.pairwise_imp_of_mem {α : Type u_1} {R T : α → α → Prop} {l : List α} (hR : List.Pairwise R l) (hT : ∀ x ∈ l, ∀ y ∈ l, R x y → T x y) : List.Pairwise T l

theorem MathlibNt.SieveTheory.SwitchingPrinciple.transformedH_suzukiFiniteNodes_increments_nonneg {D w z s σ : ℝ} {H : ℝ → ℝ} (S : BoundingSieve) (hD : 1 < D) (hw : 1 < w) (hwz : w ≤ z) (hcoord : ∀ x ∈ Set.Icc w z, Real.log D / Real.log x ∈ Set.Icc s σ) (hH : ∀ t ∈ Set.Icc s σ, 0 ≤ H t) (hHt : AntitoneOn (fun (t : ℝ) => H t * t) (Set.Icc s σ)) : List.Pairwise (fun (x y : ℝ) => 0 ≤ H (Real.log D / Real.log y) - H (Real.log D / Real.log x)) (suzukiFiniteNodes S w z)

Every forward finite-node variation increment g y - g x is nonnegative. In particular this holds for each adjacent pair used by the Abel variation sum.

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiDimensionOneError_self (S : BoundingSieve) {z : ℝ} (hz : Real.log z ≠ 0) : suzukiDimensionOneError S z z = 0

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodeAbel_mainRatio_errorVariation (S : BoundingSieve) (w z : ℝ) (g : ℝ → ℝ) : LinearSieve.finiteNodeAtomSum (fun (x : ℝ) => suzukiLocalRatio S x z) g (suzukiFiniteNodes S w z) = LinearSieve.finiteNodeMainRatioSum z g (suzukiFiniteNodes S w z) + (suzukiDimensionOneError S w z * g w - suzukiDimensionOneError S z z * g z + LinearSieve.finiteNodeVariationSum (fun (x : ℝ) => suzukiDimensionOneError S x z) g (suzukiFiniteNodes S w z))

Exact finite-node decomposition of Suzuki's local Euler ratio into its log z / log x main ratio and the dimension-one error.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSixPrimeSum_mainErrorSplit (S : BoundingSieve) (D w z : ℝ) (H : ℝ → ℝ) (hwz : w ≤ z) (hz : Real.log z ≠ 0) : suzukiLemmaEightSixPrimeSum S D w z H = LinearSieve.finiteNodeMainRatioSum z (fun (x : ℝ) => H (Real.log D / Real.log x)) (suzukiFiniteNodes S w z) + (suzukiDimensionOneError S w z * H (Real.log D / Real.log w) + LinearSieve.finiteNodeVariationSum (fun (x : ℝ) => suzukiDimensionOneError S x z) (fun (x : ℝ) => H (Real.log D / Real.log x)) (suzukiFiniteNodes S w z))

Source-faithful exact main/error split for the Suzuki Lemma 8.6 prime sum. The upper endpoint error vanishes when log z ≠ 0.

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

The finite error expression in Suzuki Lemma 8.6.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteErrorVariation S D w z H = (fun (x : ℝ) => MathlibNt.SieveTheory.SwitchingPrinciple.suzukiDimensionOneError S x z) w * (fun (x : ℝ) => H (Real.log D / Real.log x)) w + MathlibNt.SieveTheory.LinearSieve.finiteNodeVariationSum (fun (x : ℝ) => MathlibNt.SieveTheory.SwitchingPrinciple.suzukiDimensionOneError S x z) (fun (x : ℝ) => H (Real.log D / Real.log x)) (MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteNodes S w z)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiFiniteErrorVariation_le {S : BoundingSieve} {D w z s σ K : ℝ} {H : ℝ → ℝ} (hD : 1 < D) (hw2 : 2 ≤ w) (hwz : w ≤ z) (hs : 0 < s) (hsσ : s ≤ σ) (hz : z = D ^ (1 / s)) (hw : w = D ^ (1 / σ)) (hH0 : ∀ t ∈ Set.Icc s σ, 0 ≤ H t) (hHt : AntitoneOn (fun (t : ℝ) => H t * t) (Set.Icc s σ)) (hK : 0 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) : suzukiFiniteErrorVariation S D w z H ≤ 2 * K * H s / Real.log w

Suzuki Lemma 8.6's finite error-variation estimate. Only the one-sided local-product error bound is used; no absolute-value estimate for E is needed.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSixDimensionOne {S : BoundingSieve} {D w z s σ K : ℝ} {H : ℝ → ℝ} (hD : 1 < D) (hw2 : 2 ≤ w) (hs : 0 < s) (hsσ : s ≤ σ) (hz : z = D ^ (1 / s)) (hw : w = D ^ (1 / σ)) (hHcont : Continuous H) (hH0 : ∀ t ∈ Set.Icc s σ, 0 ≤ H t) (hHt : AntitoneOn (fun (t : ℝ) => H t * t) (Set.Icc s σ)) (hK : 0 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) : suzukiLemmaEightSixPrimeSum S D w z H ≤ (1 / s * ∫ (t : ℝ) in s..σ, H t) + 2 * K * H s / Real.log w

Suzuki Lemma 8.6 in dimension one, with the source-faithful main term (1/s) ∫ₛ^σ H(t) dt. It follows from the generic local Euler-product bound; no prime-specific PNT or Mertens theorem is used.