theorem MathlibNt.Analysis.eventually_log_rpow_remainder_lt_of_lower_bound (C u ρ κ : ℝ) (hu : 0 < u) (hρ : 0 < ρ) (hκ : 0 < κ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (p s : ℝ), u ≤ s → C * ↑N / Real.log ↑N ^ (p + κ) < ρ * s * ↑N / Real.log ↑N ^ p

A fixed positive logarithmic saving absorbs every fixed coefficient, uniformly in the normalization exponent and every weight with a positive uniform lower bound. The cutoff precedes both varying parameters p and s.