noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiYOne (D β : ℝ) : ℝ

Suzuki's y₁ = D^(1/(β+1)).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiYOne D β = D ^ (1 / (β + 1))

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVOneNormalized (S : BoundingSieve) (D β z : ℝ) : ℝ

The exact finite normalized base object V₁(D,z)/V(z) from Lemma 7.1:

∑_{y₁ ≤ p < z} ν(p) V(p)/V(z).

Only supported primes occur, as required by the finite BoundingSieve model. The D argument in the production prime-sum is the power-coordinate parameter; for the constant test function used here it does not affect the value.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVOneNormalized S D β z = MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSixPrimeSum S D (MathlibNt.SieveTheory.SwitchingPrinciple.suzukiYOne D β) z fun (x : ℝ) => 1

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

The finite Euler product V(z) on the production support.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S z = ∏ p ∈ S.prodPrimes.primeFactors with ↑p < z, (1 - S.nu p)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVOne (S : BoundingSieve) (D β z : ℝ) : ℝ

The unnormalized finite base object V₁(D,z). Expanding the normalized prime sum gives exactly ∑_{y₁≤p<z} ν(p)V(p).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVOne S D β z = MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S z * MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVOneNormalized S D β z

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct_pos (S : BoundingSieve) (z : ℝ) : 0 < suzukiVProduct S z

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVOneNormalized_eq_localRatio_sub_one (S : BoundingSieve) (D β z : ℝ) (hyz : suzukiYOne D β ≤ z) : suzukiVOneNormalized S D β z = suzukiLocalRatio S (suzukiYOne D β) z - 1

Suzuki Lemma 8.4 at the exact real base cutoff. The proof uses the production real-node Abel identity and prime-atom assembly. Lemma 8.6 is not needed in the base case: its integral estimate would be weaker than this exact telescoping identity.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLayer_one_eq_base_main {β s : ℝ} (hs : 0 < s) (hsβ : s ≤ β + 1) : SuzukiFiniteContinuousLayers.suzukiLayer 1 β 1 s = (β + 1 - s) / s

At κ = 1 and on the base source interval, Suzuki's continuous layer is f₁(s) = ((β+1)-s)/s.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceLayer_one_eq_suzukiLayer (β s : ℝ) : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β 1 s = SuzukiFiniteContinuousLayers.suzukiLayer 1 β 1 s

The one-term source-parity sum is exactly f₁.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLocalRatio_eq_max_two (S : BoundingSieve) (w z : ℝ) : suzukiLocalRatio S w z = suzukiLocalRatio S (max w 2) z

Replacing a real lower cutoff by max(w,2) does not change the finite Euler ratio: every member of prodPrimes.primeFactors is a prime and hence at least two. This is the exact endpoint repair used in Suzuki's base case.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVOneNormalized_le_fOne_add_localError {S : BoundingSieve} {D β z s K : ℝ} (hD : 1 < D) (hβ : 1 < β) (hs : 0 < s) (hsβ : s ≤ β + 1) (hz : z = D ^ (1 / s)) (hz2 : 2 ≤ z) (hK : 0 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) : suzukiVOneNormalized S D β z ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β 1 s + K * (β + 1) ^ 2 / (s * Real.log D)

N=1, κ=1 local-product closure.

This is the finite content of Suzuki (14.8), before the paper-specific T̂⁺ absorption: the main term is the genuine continuous f₁(s), and the remaining loss is the explicit dimension-one local-product error K(β+1)²/(s log D).

The production local-product contract starts at 2. As in Suzuki's proof, we therefore replace y₁ by max(y₁,2), use the exact carrier equality above, and then enlarge the elementary logarithmic bound back to y₁.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVOne_le_V_mul_fOne_add_localError {S : BoundingSieve} {D β z s K : ℝ} (hD : 1 < D) (hβ : 1 < β) (hs : 0 < s) (hsβ : s ≤ β + 1) (hz : z = D ^ (1 / s)) (hz2 : 2 ≤ z) (hK : 0 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) : suzukiVOne S D β z ≤ suzukiVProduct S z * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β 1 s + K * (β + 1) ^ 2 / (s * Real.log D))

Unnormalized form of the N=1 base estimate, with the exact source V(z) factor displayed.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVOneNormalized_eq_zero_of_upper (S : BoundingSieve) {D β z s : ℝ} (hD : 1 < D) (hβ : 1 < β) (hβs : β + 1 ≤ s) (hz : z = D ^ (1 / s)) : suzukiVOneNormalized S D β z = 0

The discrete base object vanishes in the support branch s ≥ β+1.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceLayer_one_eq_zero_of_upper (β : ℝ) {s : ℝ} (hs : β + 1 ≤ s) : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β 1 s = 0

Source support branch: for s ≥ β+1, the continuous f₁ vanishes.