theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kModSupport_eventually_level_le_long : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 0 < T → 4 * M * T = x → T ≤ x ^ (1 / 9) → L ≤ x ^ (5 / 9) → L ≤ M

The enlarged short-variable range still pays the progression endpoint.