noncomputable def MathlibNt.SieveTheory.caseIIRoundedProductTransportCoeff (K yr : ℝ) : ℝ

Product-ratio coefficient written at the real cubic coordinate.

Equations

• MathlibNt.SieveTheory.caseIIRoundedProductTransportCoeff K yr = 1 + K / Real.log yr

noncomputable def MathlibNt.SieveTheory.caseIIRoundedLogTransportCoeff (zr : ℝ) : ℝ

Reciprocal logarithmic transport coefficient written at the real target coordinate. In the rounded route this is evaluated at zr = D^(1/s), never at the cast of its natural ceiling.

Equations

• MathlibNt.SieveTheory.caseIIRoundedLogTransportCoeff zr = 1 / Real.log zr

noncomputable def MathlibNt.SieveTheory.caseIIRoundedFiniteEndpointCorrections (N : ℕ) (D d Δ σ C K s zr : ℝ) : ℝ

The finite (non-integral) rounded endpoint corrections. Division by s is paired with 1 / log zr; after zr = D^(1/s) this is exactly division by log D.

Equations

• MathlibNt.SieveTheory.caseIIRoundedFiniteEndpointCorrections N D d Δ σ C K s zr = (MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeffA0 N K + σ * MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeffA1 N K) / s * MathlibNt.SieveTheory.caseIIRoundedLogTransportCoeff zr + σ * MathlibNt.SieveTheory.caseIIQDEndpointCoeffA0 d Δ C K / s * MathlibNt.SieveTheory.caseIIRoundedLogTransportCoeff zr * Real.log D ^ (-Δ)

noncomputable def MathlibNt.SieveTheory.caseIIRoundedEndpointErr (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N D z : ℕ) (yr zr d Δ σ C K B0 s : ℝ) : ℝ

Rounded Case-II endpoint error. Analytic coordinates yr,zr are real, while the Euler product retains the natural ceiling carrier z.

Equations

• MathlibNt.SieveTheory.caseIIRoundedEndpointErr S H N D z yr zr d Δ σ C K B0 s = B0 + MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * (MathlibNt.SieveTheory.caseIIPositiveDeltaIntegralPart H N (↑D) yr d Δ σ C K s + MathlibNt.SieveTheory.caseIIRoundedFiniteEndpointCorrections N (↑D) d Δ σ C K s zr)

theorem MathlibNt.SieveTheory.nat_lt_natCeil_iff {x : ℝ} {z p : ℕ} (hz : z = ⌈x⌉₊) : p < z ↔ ↑p < x

A strict cutoff at a real number has the same natural carrier as a strict cutoff at its natural ceiling.

theorem MathlibNt.SieveTheory.suzukiVProduct_natCeil_real_eq (S : BoundingSieve) {x : ℝ} {z : ℕ} (hz : z = ⌈x⌉₊) : SwitchingPrinciple.suzukiVProduct S ↑z = SwitchingPrinciple.suzukiVProduct S x

Euler products are literally unchanged by replacing a strict real cutoff with its natural ceiling.

theorem MathlibNt.SieveTheory.caseIIRoundedProductTransportCoeff_cuberoot {D K yr : ℝ} (hD : 0 < D) (hyr : yr = D ^ (1 / 3)) : caseIIRoundedProductTransportCoeff K yr = 1 + 3 * K / Real.log D

At the real cubic coordinate, the product-ratio coefficient has the exact 1 + 3K/log D form.

theorem MathlibNt.SieveTheory.caseIIRoundedIntegralPart_source_relative (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N : ℕ} {D yr d Δ σ C K s : ℝ} (hyr : yr = D ^ (1 / 3)) (hD : 1 < D) (hs : 0 < s) (hC : 0 ≤ C) (hK : 0 ≤ K) (hcut : 0 ≤ (1 - 1 / σ) ^ (1 - Δ)) (hiii : ∫ (t : ℝ) in 3..σ, SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite D d Δ t ≤ (1 - 1 / σ) ^ (1 - Δ) * SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) D d 0 3) (hcubic : SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) D d 0 3 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d 0 3 * SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) D d 0 s) : caseIIPositiveDeltaIntegralPart H N D yr d Δ σ C K s ≤ C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s * Real.log D ^ (-Δ) * ((1 + 3 * K / Real.log D) * (1 - 1 / σ) ^ (1 - Δ) * SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d 0 3)

The rounded integral term is bounded at the genuine real cubic coordinate. No equality between the cube root and the cast of its ceiling is needed.

theorem MathlibNt.SieveTheory.caseIIRoundedLogTransportCoeff_rpow {D s zr : ℝ} (hD : 0 < D) (hs : s ≠ 0) (hzr : zr = D ^ (1 / s)) : caseIIRoundedLogTransportCoeff zr = s / Real.log D

At the real target coordinate, reciprocal-log transport is exactly s/log D.

theorem MathlibNt.SieveTheory.caseIIRoundedFiniteEndpointCorrections_eq_logD {N : ℕ} {D d Δ σ C K s zr : ℝ} (hD : 0 < D) (hs : s ≠ 0) (hzr : zr = D ^ (1 / s)) : caseIIRoundedFiniteEndpointCorrections N D d Δ σ C K s zr = (caseIIAlgebraicEndpointCoeffA0 N K + σ * caseIIAlgebraicEndpointCoeffA1 N K) / Real.log D + σ * caseIIQDEndpointCoeffA0 d Δ C K / Real.log D * Real.log D ^ (-Δ)

The two finite rounded corrections are exactly the production log D terms. In particular this proof uses log (D^(1/s)), not log ((ceil (D^(1/s)) : ℕ) : ℝ).

theorem MathlibNt.SieveTheory.caseIIRoundedEndpointErr_eq_realTransport (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D z : ℕ} {yr zr d Δ σ C K B0 s : ℝ} (hz : z = ⌈zr⌉₊) : caseIIRoundedEndpointErr S H N D z yr zr d Δ σ C K B0 s = B0 + SwitchingPrinciple.suzukiVProduct S zr * (caseIIPositiveDeltaIntegralPart H N (↑D) yr d Δ σ C K s + caseIIRoundedFiniteEndpointCorrections N (↑D) d Δ σ C K s zr)

Exact transport expansion of the rounded error with the real Euler product. The only use of the natural rounded target is the carrier identity.

theorem MathlibNt.SieveTheory.caseIIRoundedEndpointErr_eq_logD_realProduct (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D z : ℕ} {yr zr d Δ σ C K B0 s : ℝ} (hD : 0 < ↑D) (hs : s ≠ 0) (hzr : zr = ↑D ^ (1 / s)) (hz : z = ⌈zr⌉₊) : caseIIRoundedEndpointErr S H N D z yr zr d Δ σ C K B0 s = B0 + SwitchingPrinciple.suzukiVProduct S zr * (caseIIPositiveDeltaIntegralPart H N (↑D) yr d Δ σ C K s + (caseIIAlgebraicEndpointCoeffA0 N K + σ * caseIIAlgebraicEndpointCoeffA1 N K) / Real.log ↑D + σ * caseIIQDEndpointCoeffA0 d Δ C K / Real.log ↑D * Real.log ↑D ^ (-Δ))

Exact log/product transport expansion when both real coordinates are the prescribed powers and the target Euler carrier is their natural ceiling.

theorem MathlibNt.SieveTheory.caseII_rounded_positiveDelta_relative_packet_fixed_coefficients (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D z : ℕ} {yr zr d Δ σ C K B0 s : ℝ} (hD : 1 < ↑D) (_hΔ0 : 0 < Δ) (_hΔ1 : Δ < 1) (hs1 : 1 < s) (hK : 0 ≤ K) (hE : 1 / 3 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s) (hzr : zr = ↑D ^ (1 / s)) : caseIIRoundedEndpointErr S H N D z yr zr 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) yr d Δ σ C K s + (caseIIAlgebraicEndpointCoeffA0 N K * Real.log ↑D ^ (Δ - 1) + σ * caseIIAlgebraicEndpointCoeffA1 N K * Real.log ↑D ^ (Δ - 1) + σ * caseIIQDEndpointCoeffA0 d Δ C K / Real.log ↑D + 27 * K * Real.log ↑D ^ (Δ - 1) * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s) * Real.log ↑D ^ (-Δ))

Positive-Δ rounded relative packet with fixed coefficients. The algebraic and cubic-q_D terms do not acquire an error-envelope factor; only the sharp raw-base correction does.