theorem MathlibNt.SieveTheory.tendsto_caseI1423_sourceScalar (K d Δ : ℝ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : Filter.Tendsto (fun (D : ℝ) => K ^ 2 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ^ 3 * Real.log (Real.exp 1 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) * Real.log (Real.log D) / Real.log D ^ (1 - Δ)) Filter.atTop (nhds 0)

The literal σ³ log (eσ) scalar in (14.23) tends to zero in the Case-I range. This uses the explicit definition of sourceSigma; no limit statement is assumed.

theorem MathlibNt.SieveTheory.caseI1423Sigma11SourceScalar_of_range (K d Δ : ℝ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : CaseI1423Sigma11SourceScalar K d Δ

Boundedness form required by the Σ₁₁ endpoint source contract.

theorem MathlibNt.SieveTheory.caseI1423Sigma12SourceScalar_of_range (K d Δ : ℝ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : CaseI1423Sigma12SourceScalar K d Δ

The Σ₁₂ source contract has the same literal scalar and follows from the same decay theorem.