English
If the derivative of f is temperate growth as a function, then f itself has temperate growth provided f is differentiable and a linear bound on ‖f(x)‖ holds with a polynomial weight.
Русский
Если производная f имеет темперированный рост и f дифференцируема, а также существует полиномиальная граница на ‖f(x)‖, то f тоже имеет темперированный рост.
LaTeX
$$$\\text{HasTemperateGrowth}(f)\\Leftarrow\\text{HasTemperateGrowth}(fderiv) \\wedge \\text{Differentiable}(f) \\wedge (\\exists k, C\\ge 0: \\forall x, \\|f(x)\\| ≤ C(1+\\|x\\|)^k).$$$
Lean4
theorem _root_.Function.HasTemperateGrowth.of_fderiv {f : E → F} (h'f : Function.HasTemperateGrowth (fderiv ℝ f))
(hf : Differentiable ℝ f) {k : ℕ} {C : ℝ} (h : ∀ x, ‖f x‖ ≤ C * (1 + ‖x‖) ^ k) : Function.HasTemperateGrowth f :=
by
refine ⟨contDiff_succ_iff_fderiv.2 ⟨hf, by simp, h'f.1⟩, fun n ↦ ?_⟩
rcases n with rfl | m
· exact ⟨k, C, fun x ↦ by simpa using h x⟩
· rcases h'f.2 m with ⟨k', C', h'⟩
refine ⟨k', C', ?_⟩
simpa [iteratedFDeriv_succ_eq_comp_right] using h'
