Theorem Function.HasTemperateGrowth.isBigO

Modification history

2025-10-29 13:18
Mathlib/Analysis/Distribution/SchwartzSpace.lean
chore(Analysis/Distribution): split off functions and measures of temperate growth (#30553) …
Modified Function.HasTemperateGrowth.isBigOView on Github →
2025-10-09 12:15
Mathlib/Analysis/Distribution/SchwartzSpace.lean
feat: interpret `HasTemperateGrowth` in terms of `IsBigO` (#30251) …
Added Function.HasTemperateGrowth.isBigOView on Github →