theorem MathlibNt.SieveTheory.LiLiuPrereqWF.G9ExtendedUpper.upper_bounded {s : ℝ} (hs : 1 / 2 ≤ s) (hs3 : s ≤ 3) : 0 ≤ JurkatRichert1965ChenGammaOneQOne.jr1965F s ∧ JurkatRichert1965ChenGammaOneQOne.jr1965F s ≤ 2 * JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.G9ExtendedUpper.small_dimension_scalar {ε L K C r s : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8) (hL : 1 ≤ L) (hK : 0 ≤ K) (hKL : K ≤ L) (hC : 0 ≤ C) (hr : 0 ≤ r) (hr8 : r ≤ 8) (hs : 1 / 2 ≤ s) (hsc : s ≤ 2 * (1 + ε + ε ^ 9)) (hid : JurkatRichert1965ChenGammaOneQOne.jr1965F 2 * r = JurkatRichert1965ChenGammaOneQOne.jr1965F s * (1 + ε + ε ^ 9)) : (JurkatRichert1965ChenGammaOneQOne.jr1965F 2 + C * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * L ^ (-(1 / 3)))) * r * (1 + 2 * K / L) ≤ JurkatRichert1965ChenGammaOneQOne.jr1965F s + (24 * C + 12 * JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant) * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * L ^ (-(1 / 3)))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.G9ExtendedUpper.large_dimension_scalar {a ε x y K : ℝ} (ha : 0 < a) (hε : 0 < ε) (hε1 : ε ≤ 1) (hx : 1 ≤ x) (hy : 0 ≤ y) (hyx : y ≤ 4 * x) (hxK : x ≤ K) : (y / a * (1 + K / a)) ^ 2 ≤ 16 * (1 / a * (1 + 1 / a)) ^ 2 * ((ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * x ^ (-(1 / 3)))