Exact integer-level transport of the actual small weights

The natural level is ceil L, not floor L + 1: every test in the coefficients is a strict comparison of an integer with the real level. The rounded cutoff is matched using s = log (ceil L) / log u.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.nat_lt_real_iff_lt_ceil (n : ℕ) (L : ℝ) : ↑n < L ↔ ↑n < ↑⌈L⌉₊

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.integer_cubic_lt_ceil (m p : ℕ) (L : ℝ) (k : ℕ) : ↑m * ↑p ^ k < L ↔ ↑m * ↑p ^ k < ↑⌈L⌉₊

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerAdmissibleSet_ceil (L : ℝ) (s : Finset ℕ) : LowerAdmissibleSet (↑⌈L⌉₊) s ↔ LowerAdmissibleSet L s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperAdmissibleSet_ceil (L : ℝ) (s : Finset ℕ) : UpperAdmissibleSet (↑⌈L⌉₊) s ↔ UpperAdmissibleSet L s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_ceil (M : ℕ) (L : ℝ) : lowerWeight M ↑⌈L⌉₊ = lowerWeight M L

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_ceil (M : ℕ) (L : ℝ) : upperWeight M ↑⌈L⌉₊ = upperWeight M L

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.setWeight_ceil (L : ℝ) (s : Finset ℕ) : setWeight (↑⌈L⌉₊) s = setWeight L s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetWeight_ceil (L : ℝ) (s : Finset ℕ) : upperSetWeight (↑⌈L⌉₊) s = upperSetWeight L s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerBoundary_ceil (L : ℝ) (q : ℕ) (s : Finset ℕ) : LowerBoundary (↑⌈L⌉₊) q s ↔ LowerBoundary L q s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperBoundary_ceil (L : ℝ) (q : ℕ) (s : Finset ℕ) : UpperBoundary (↑⌈L⌉₊) q s ↔ UpperBoundary L q s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.densityDefects_ceil (L : ℝ) (g : ℕ → ℝ) (ps : List ℕ) : lowerDensityDefect (↑⌈L⌉₊) g ps = lowerDensityDefect L g ps ∧ upperDensityDefect (↑⌈L⌉₊) g ps = upperDensityDefect L g ps

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.roundedSieveCoordinate (L u : ℝ) : ℝ

The coordinate uses the rounded level but the original real cutoff.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.roundedSieveCoordinate L u = Real.log ↑⌈L⌉₊ / Real.log u

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.roundedSieveCoordinate_pos {L u : ℝ} (hL : 1 < L) (hu : 1 < u) : 0 < roundedSieveCoordinate L u

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.roundedSieveCoordinate_cutoff {L u : ℝ} (hL : 1 < L) (hu : 1 < u) : ↑⌈L⌉₊ ^ (1 / roundedSieveCoordinate L u) = u

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.roundedSieveCoordinate_prime_cutoff {L u : ℝ} (hL : 1 < L) (hu : 1 < u) (p : ℕ) : p < ⌈↑⌈L⌉₊ ^ (1 / roundedSieveCoordinate L u)⌉₊ ↔ ↑p < u

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.roundedSieveCoordinate_carrier (P : Finset ℕ) {L u : ℝ} (hL : 1 < L) (hu : 1 < u) : {p ∈ P | Nat.Prime p ∧ p < ⌈↑⌈L⌉₊ ^ (1 / roundedSieveCoordinate L u)⌉₊} = {p ∈ P | Nat.Prime p ∧ ↑p < u}

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.small_rounded_cutoff_bounds {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hε1 : ε ≤ 1) : 2 ≤ ⌈D ^ ε ^ 2⌉₊ ∧ ⌈D ^ ε ^ 2⌉₊ ≤ ⌈D ^ ε⌉₊