noncomputable def MathlibNt.SieveTheory.caseIIPositiveDeltaIntegralPart (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N : ℕ) (D y d Δ σ C K s : ℝ) : ℝ

The Claim-14.6(iii) integral contribution in the transported Case-II endpoint. It is kept separate from all finite endpoint corrections.

Equations

• MathlibNt.SieveTheory.caseIIPositiveDeltaIntegralPart H N D y d Δ σ C K s = 3 / s * (1 + K / Real.log y) * (C * Real.exp √K * Real.log D ^ (-Δ) * (1 / 3 * ∫ (t : ℝ) in 3..σ, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite D d Δ t))

theorem MathlibNt.SieveTheory.caseIIEndpointErr_eq_positiveDelta_packet_expansion (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D y z : ℕ} {w d Δ σ C K B0 s : ℝ} (hw : w = ↑D ^ (1 / σ)) : caseIIEndpointErr S H N D y z d Δ σ C K B0 s = B0 + SwitchingPrinciple.suzukiVProduct S ↑z * (caseIIPositiveDeltaIntegralPart H N (↑D) (↑y) d Δ σ C K s + SwitchingPrinciple.SuzukiLemma144KappaOne.caseIINonIntegralEndpointCorrections H N (↑D) (↑y) w d Δ σ C K s)

Exact expansion of caseIIEndpointErr used by the positive-Δ packet. The algebraic and q_D(3) endpoint terms are not merged: their distinct logarithmic scales remain visible.

theorem MathlibNt.SieveTheory.caseII_positiveDelta_relative_endpoint_packet (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D y z : ℕ} {w d Δ σ C K B0 s : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) (hN : Odd N) (hD : Real.exp 1 ≤ ↑D) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hy : ↑y = ↑D ^ (1 / 3)) (hw : w = ↑D ^ (1 / σ)) (hσ : 0 < σ) (hs1 : 1 < s) (hs3 : s ≤ 3) (hK : 0 ≤ K) (hC : 0 ≤ C) (hsmall : 3 ^ d ≤ Real.log ↑D) : caseIIEndpointErr S H N D y z d Δ σ C K B0 s + SwitchingPrinciple.suzukiVProduct S ↑z * (K * 3 ^ 2 / (s * Real.log ↑D)) ≤ B0 + SwitchingPrinciple.suzukiVProduct S ↑z * (caseIIPositiveDeltaIntegralPart H N (↑D) (↑y) d Δ σ C K s + (SwitchingPrinciple.SuzukiLemma144KappaOne.caseIIAlgebraicEndpointCoeff N σ K * Real.log ↑D ^ (Δ - 1) + SwitchingPrinciple.SuzukiLemma144KappaOne.caseIIQDEndpointCoeff d Δ σ C K / Real.log ↑D + 27 * K * Real.log ↑D ^ (Δ - 1) * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s) * Real.log ↑D ^ (-Δ))

Source-positive-Δ relative Case-II endpoint packet.

For 0 < Δ < 1, the two finite endpoint scales and the sharp source-base loss are retained exactly as

• A * (log D)^(Δ-1) for the algebraic endpoint terms;
• Aq / log D for the cubic q_D(3) endpoint term;
• 27 K * (log D)^(Δ-1) * errorEnvelope for the sharp raw base term.

Thus no coefficient is prematurely replaced by a constant. In particular, this statement uses neither an artificial hScale : 1 ≤ (log D)^(-Δ) nor a nonpositive-Δ hypothesis.