Commit 2025-11-05 05:40 02e01097

View on Github →

feat(Analysis/Distribution): basic algebraic properties of functions of temperate growth (#31112)

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Lemmas.lean

added theorem Asymptotics.IsBigO.pow_of_le_right

Modified Mathlib/Analysis/Calculus/ContDiff/Operations.lean

added theorem iteratedFDeriv_add

added theorem iteratedFDeriv_neg

Modified Mathlib/Analysis/Distribution/TemperateGrowth.lean

added theorem Function.HasTemperateGrowth.add

added theorem Function.HasTemperateGrowth.neg

added theorem Function.HasTemperateGrowth.sub