noncomputable def MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeffSourceLarge (N : ℕ) (D σ K : ℝ) : ℝ

The algebraic endpoint coefficient with the exact cubic product ratio retained. This scale-free definition lives upstream of both the rounded transport bridge and the source-large uniform cutoff.

Equations

• MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeffSourceLarge N D σ K = 9 * K * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3 + 18 * K ^ 2 * σ * (1 + 3 * K / Real.log D) * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2

noncomputable def MathlibNt.SieveTheory.caseIIQDRelativeEndpointCoeffSourceLarge (D Δ K : ℝ) : ℝ

The C-independent cubic q_D(3) relative coefficient, retaining the exact source factor 1 + 3K/log D.

Equations

• MathlibNt.SieveTheory.caseIIQDRelativeEndpointCoeffSourceLarge D Δ K = 216 * K ^ 2 * (1 + 3 * K / Real.log D) * (3 / 2) ^ Δ

noncomputable def MathlibNt.SieveTheory.caseIIEndpointRelativeCoeffSourceLarge (N : ℕ) (D Δ σ K : ℝ) : ℝ

Positive finite endpoint terms used by the source-large-log Case-II producer.

Equations

• MathlibNt.SieveTheory.caseIIEndpointRelativeCoeffSourceLarge N D Δ σ K = MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeffSourceLarge N D σ K * Real.log D ^ (Δ - 1) + σ * MathlibNt.SieveTheory.caseIIQDRelativeEndpointCoeffSourceLarge D Δ K / Real.log D + 27 * K * Real.log D ^ (Δ - 1)