Commit 2023-11-18 21:30 1d2d1d0e

View on Github →

feat(NormedSpace/FiniteDimension): add IsBigO.comp_summable (#8359) Add Asymptotics.IsBigO.comp_summable.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

added theorem Asymptotics.IsBigO.comp_summable_norm

modified theorem summable_of_isBigO

modified theorem summable_of_isBigO_nat

Modified Mathlib/Analysis/NormedSpace/FiniteDimension.lean

added theorem Asymptotics.IsBigO.comp_summable