Parameters for the rounded, moving-range density estimate

The coordinate depends on D, ε only, never on a prime carrier, density, or truncation depth. Increasing the product constant to max K 2 incurs the displayed absolute factor in exp (sqrt K).

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.dimensionOneProductBound_mono {P : Finset ℕ} {g : ℕ → ℝ} {K K' : ℝ} (h : DimensionOneProductBound P g K) (hKK : K ≤ K') : DimensionOneProductBound P g K'

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.exp_sqrt_max_two_le (K : ℝ) : Real.exp √(max K 2) ≤ Real.exp √2 * Real.exp √K

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.log_ceil_rpow_bounds {D ε : ℝ} (hD : 2 ≤ D) (hlarge : Real.log 2 ≤ ε * Real.log D) : ε * Real.log D ≤ Real.log ↑⌈D ^ ε⌉₊ ∧ Real.log ↑⌈D ^ ε⌉₊ ≤ 2 * (ε * Real.log D)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.small_roundedSieveCoordinate_bounds {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hlarge : Real.log 2 ≤ ε * Real.log D) : 1 / ε ≤ roundedSieveCoordinate (D ^ ε) (D ^ ε ^ 2) ∧ roundedSieveCoordinate (D ^ ε) (D ^ ε ^ 2) ≤ 2 / ε

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.small_rounded_power_budget {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hlarge : max (Real.log 2) ((2 / ε) ^ 13) ≤ ε * Real.log D) : roundedSieveCoordinate (D ^ ε) (D ^ ε ^ 2) ^ 13 ≤ Real.log ↑⌈D ^ ε⌉₊

A fixed numerical threshold gives the power budget uniformly in all subsequently chosen sieve data and depths.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.moving_envelope_le_exp_one {t s : ℝ} (hs : 0 < s) (ht : s ^ 13 ≤ t) : (1 + s ^ 12 / t) ^ s ≤ Real.exp 1

The precise s in the moving-range envelope is retained.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.moving_range_of_power_budget {R s : ℝ} (hR : 0 < R) (hs : 1 ≤ s) (hbudget : s ^ 13 ≤ Real.log R) (hlog : Real.exp 1 ≤ Real.log R) : s ≤ Real.log R ^ (1 / 12) * Real.log (Real.log (27 * R))

The actual shape of the source's moving endpoint, with d = 12.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.small_rounded_moving_range {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hlarge : max (max (Real.log 2) ((2 / ε) ^ 13)) (Real.exp 1) ≤ ε * Real.log D) : have R := ↑⌈D ^ ε⌉₊; have s := roundedSieveCoordinate (D ^ ε) (D ^ ε ^ 2); 8 < s ∧ s ≤ Real.log R ^ (1 / 12) * Real.log (Real.log (27 * R)) ∧ (1 + s ^ 12 / Real.log R) ^ s ≤ Real.exp 1

Explicit threshold, before all carriers, densities, and depths. Both the source domain and its envelope use the rounded coordinate.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.exists_small_rounded_moving_threshold {ε : ℝ} (hε : 0 < ε) (hεsmall : ε < 1 / 8) : ∃ (D₀ : ℝ), 2 ≤ D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → have R := ↑⌈D ^ ε⌉₊; have s := roundedSieveCoordinate (D ^ ε) (D ^ ε ^ 2); 8 < s ∧ s ≤ Real.log R ^ (1 / 12) * Real.log (Real.log (27 * R)) ∧ (1 + s ^ 12 / Real.log R) ^ s ≤ Real.exp 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.small_rounded_decay_bounds {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hlarge : Real.log 2 ≤ ε * Real.log D) : Real.exp (-roundedSieveCoordinate (D ^ ε) (D ^ ε ^ 2)) ≤ Real.exp (-(1 / ε)) ∧ Real.log ↑⌈D ^ ε⌉₊ ^ (-(1 / 3)) ≤ (ε * Real.log D) ^ (-(1 / 3))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.small_rounded_error_bound (A B K : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hlarge : Real.log 2 ≤ ε * Real.log D) : have s := roundedSieveCoordinate (D ^ ε) (D ^ ε ^ 2); A * Real.exp (-s) + B * Real.exp √(max K 2) * Real.exp (-s) * Real.log ↑⌈D ^ ε⌉₊ ^ (-(1 / 3)) ≤ max A (B * Real.exp √2) * (Real.exp (-(1 / ε)) + Real.exp (√K - 1 / ε) * (ε * Real.log D) ^ (-(1 / 3)))

Transport the two terms of the rounded producer error to the original parameters. The constant is independent of K, D, and ε.