Commit 2025-01-05 13:11 9173268a

View on Github →

feat(Asymptotics): add Asymptotics.*.*Prod lemmas (#20458) IsBigO.fisnetProd comes from https://github.com/urkud/SardMoreira, the others are added to avoid gaps in the API.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

deleted theorem Asymptotics.IsEquivalent.div

added theorem Asymptotics.IsEquivalent.finsetProd

deleted theorem Asymptotics.IsEquivalent.inv

added theorem Asymptotics.IsEquivalent.listProd

deleted theorem Asymptotics.IsEquivalent.mul

added theorem Asymptotics.IsEquivalent.multisetProd

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

added theorem Asymptotics.IsBigO.finsetProd

added theorem Asymptotics.IsBigO.listProd

added theorem Asymptotics.IsBigO.multisetProd

added theorem Asymptotics.IsLittleO.finsetProd

added theorem Asymptotics.IsLittleO.listProd

added theorem Asymptotics.IsLittleO.multisetProd

Modified Mathlib/Analysis/Asymptotics/Theta.lean

added theorem Asymptotics.IsTheta.finsetProd

added theorem Asymptotics.IsTheta.listProd

added theorem Asymptotics.IsTheta.multisetProd