noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9PrimeHalfOpenInterval (T L U : ℝ) (hT : 3 ≤ T) (hTL : T ≤ L) (hLU : L ≤ U) (hUT : U ≤ 4 / 3 * T) : PrimeC2Interval

Encode the integer points of [L,U) in the existing (lower,upper] prime family. Buffering the scale avoids deleting an integral left endpoint.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9PrimeHalfOpenInterval T L U hT hTL hLU hUT = { scale := 2 / 3 * T, lower := ↑⌈L⌉ - 1, upper := ↑⌈U⌉ - 1, one_le_scale := ⋯, scale_le_lower := ⋯, lower_le_upper := ⋯, upper_le_twice := ⋯ }

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_g9PrimeHalfOpenInterval (T L U : ℝ) (hT : 3 ≤ T) (hTL : T ≤ L) (hLU : L ≤ U) (hUT : U ≤ 4 / 3 * T) (n : ℕ) : have z := g9PrimeHalfOpenInterval T L U hT hTL hLU hUT; n ∈ primeSWInterval z.lower z.upper ↔ L ≤ ↑n ∧ ↑n < U

Both endpoint conventions are exact, including integral L or U.