theorem MathlibNt.SieveTheory.LiuWeight.eventually_inverse_log_remainder_le_liuSingularSeries (C ρ : ℝ) (hρ : 0 < ρ) : ∀ᶠ (N : ℕ) in Filter.atTop, C * ↑N / Real.log ↑N ^ 3 ≤ ρ * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

An inverse-log remainder is absorbed into an arbitrary positive multiple of the genuine Liu singular-series scale. The uniform lower bound is the positive universal Euler product, since every divisor correction factor is at least one.