theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable.level_mono {k : ℕ} {L L' : ℝ} {c : ℕ → ℝ} (hc : SignedWellFactorable k L c) (hL : 1 ≤ L) (hLL' : L ≤ L') : SignedWellFactorable k L' c

Transport the same weight to a larger factorization level. No restriction or mask is applied to the weight; every split of the new level is covered.