A single internal level for a prescribed external level

The internal level is chosen before every factorization and every sieve datum. The logarithmic error is transported without changing the original K.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel (Q ε : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q ε = Q ^ (1 + ε + ε ^ 9)⁻¹

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.external_dilation_bounds {ε : ℝ} (hε : 0 < ε) (hεsmall : ε < 1 / 8) : 1 < 1 + ε + ε ^ 9 ∧ 1 + ε + ε ^ 9 ≤ 1 + 2 * ε ∧ 1 + ε + ε ^ 9 < 3 / 2

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel_pos {Q ε : ℝ} (hQ : 0 < Q) : 0 < externalInternalLevel Q ε

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel_level {Q ε : ℝ} (hQ : 0 ≤ Q) (hε : 0 < ε) (hεsmall : ε < 1 / 8) : externalInternalLevel Q ε ^ (1 + ε + ε ^ 9) = Q

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel_log {Q ε : ℝ} (hQ : 0 < Q) : Real.log (externalInternalLevel Q ε) = Real.log Q / (1 + ε + ε ^ 9)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel_ge_threshold {D₀ Q ε : ℝ} (hD₀ : 0 ≤ D₀) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hQ : D₀ ^ (1 + ε + ε ^ 9) ≤ Q) : D₀ ≤ externalInternalLevel Q ε

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel_coordinate {Q ε z : ℝ} (hQ : 0 < Q) (hε : 0 < ε) (hεsmall : ε < 1 / 8) : Real.log Q / Real.log z = (1 + ε + ε ^ 9) * (Real.log (externalInternalLevel Q ε) / Real.log z)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sieve_coordinate_ge_two {Q z : ℝ} (hQ : 0 < Q) (hz : 2 ≤ z) (hzQ : z ≤ √Q) : 2 ≤ Real.log Q / Real.log z

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.external_edge_coordinate {Q ε z : ℝ} (hQ : 1 < Q) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hz : 2 ≤ z) (hzQ : z ≤ √Q) (hedge : √(externalInternalLevel Q ε) < z) : 2 ≤ Real.log Q / Real.log z ∧ Real.log Q / Real.log z < 2 * (1 + ε + ε ^ 9)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel_error {Q ε K : ℝ} (hQ : 1 < Q) (hε : 0 < ε) (hεsmall : ε < 1 / 8) : ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log (externalInternalLevel Q ε) ^ (-(1 / 3)) ≤ 2 * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3)))

The factor two is absolute and the exponential keeps the SAME K.