Commit 2026-06-04 20:35 632c766e

feat(Tactic/ComputeAsymptotics/Multiseries): compute limits of Monomials (#37415) Prove

• UnitMonomial.logToFun_isEquivalent_of_nonzero_head: log m.toFun is asymptotically equivalent to its first summand - m[0] • log basis[0] if m[0] ≠ 0. Using this theorem we can prove that the asymptotic behavior of a monomial is determined by its first non-zero exponent.
• toFun_tendsto_top_of_FirstNonzeroIsPos and its variants: used to infer the limit of t.toFun from FirstNonzeroIsPos/FirstNonzeroIsNeg/AllZero.
• IsLittleO_of_lt_exps and its variants: used to asymptotically compare two monomials.