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

The three non-integral pieces of the transported Case-II endpoint error, with the integral in caseIIEndpointQD omitted. The power coordinates are kept as real variables so that their exact logarithmic identities can be used.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseIINonIntegralEndpointCorrections H N D y w d Δ _σ C K s = 3 / s * (K / Real.log y) * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3 + 3 / s * (1 + K / Real.log y) * (6 * K ^ 2 * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2 / Real.log w * (3 / 3)) + 3 / s * (1 + K / Real.log y) * (C * Real.exp √K * Real.log D ^ (-Δ) * (6 * K ^ 2 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite D d Δ 3 / Real.log w * (3 / 3)))

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseIIAlgebraicEndpointCoeff (N : ℕ) (σ K : ℝ) : ℝ

A named coefficient for the two endpoint terms which do not intrinsically carry the factor (log D)^(-Δ).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseIIAlgebraicEndpointCoeff N σ K = 9 * K * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3 + 18 * K ^ 2 * σ * (1 + 3 * K) * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseIIQDEndpointCoeff (_d Δ σ C K : ℝ) : ℝ

A named coefficient for the cubic q_D(3)/log w endpoint term.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseIIQDEndpointCoeff _d Δ σ C K = 72 * K ^ 2 * σ * (1 + 3 * K) * C * Real.exp √K * (3 / 2) ^ Δ

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseII_nonIntegral_endpoint_corrections_separate {H : Section13HatLayers} {N : ℕ} {D y w d Δ σ C K s : ℝ} (hH : Section13HatContract H 2) (hN : Odd N) (hD : Real.exp 1 ≤ D) (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) : 3 / s * (K / Real.log y) * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3 + 3 / s * (1 + K / Real.log y) * (6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2 / Real.log w * (3 / 3)) ≤ caseIIAlgebraicEndpointCoeff N σ K / Real.log D ∧ 3 / s * (1 + K / Real.log y) * (C * Real.exp √K * Real.log D ^ (-Δ) * (6 * K ^ 2 * qD H (ErrorSign.ofDepth N).opposite D d Δ 3 / Real.log w * (3 / 3))) ≤ caseIIQDEndpointCoeff d Δ σ C K / Real.log D * Real.log D ^ (-Δ)

Exact, uniform estimates for all three non-integral endpoint corrections.

The first conclusion is the sharp scale actually supplied by the product-ratio and Σ₁₁ terms, namely 1 / log D. The second conclusion has the additional (log D)^(-Δ) because that factor is present in caseIIEndpointQD itself.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseII_nonIntegral_endpoint_corrections_absorb {H : Section13HatLayers} {N : ℕ} {D y w d Δ σ C K s : ℝ} (hH : Section13HatContract H 2) (hN : Odd N) (hD : Real.exp 1 ≤ D) (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) (hScale : 1 ≤ Real.log D ^ (-Δ)) : caseIINonIntegralEndpointCorrections H N D y w d Δ σ C K s ≤ 3 * (caseIIAlgebraicEndpointCoeff N σ K + caseIIQDEndpointCoeff d Δ σ C K) / Real.log D * errorEnvelope H N D d s * Real.log D ^ (-Δ)

Combining the preceding exact estimates with the odd Case-II lower bound for errorEnvelope. The extra premise is displayed because it is precisely what is needed to put the product-ratio and Σ₁₁ terms at the stronger (log D)^(-1-Δ) scale.