zero — Mathlib

English

The zero function has temperate growth, since all derivatives vanish and bounds are trivially satisfied.

Русский

Нулевая функция имеет темперированный рост, поскольку все её производные равны нулю и ограничения тривиальны.

LaTeX

$$$f(x)\\equiv 0\\;\\Rightarrow\\; fHasTemperateGrowth$.$$

Lean4

theorem _root_.Function.HasTemperateGrowth.zero : Function.HasTemperateGrowth (fun _ : E ↦ (0 : F)) :=
  by
  refine ⟨contDiff_const, fun n ↦ ⟨0, 0, fun x ↦ ?_⟩⟩
  simp only [iteratedFDeriv_zero_fun, Pi.zero_apply, norm_zero]
  positivity

Похожие утверждения