Commit 2024-12-27 09:22 5ed97c4e

View on Github →

chore(Integral/Asymptotics): drop noop _root_.Asymptotics (#20253) They're inside namespace Asymptotics.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Asymptotics.lean

modified theorem Asymptotics.IsBigO.integrable

modified theorem Asymptotics.IsBigO.integrableAtFilter