Commit 2026-02-25 20:25 c4c9be4a
View on Github →feat: asymptotic lemmas on the cobounded filter (#34920)
Actually includes one cofinite lemma too. As shown in the second commit, this allows proving what I initially proved with the help of Harmonic in #34845 in a much shorter, AI-free form.
Asymptotics.isLittleO_pow_pow_cobounded_of_lt was generalised with the help of @sgouezel – see [#PR reviews > #34868 – more general polynomial asymptotics @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2334868.20.E2.80.93.20more.20general.20polynomial.20asymptotics/near/572197174).