hasTemperateGrowth — Mathlib

English

For a continuous linear map f: E →L F, the temperate growth of f follows from standard bounds on its operator norm, yielding HasTemperateGrowth.

Русский

Для непрерывного линейного отображения f: E →L F темперированный рост следует из стандартных ограничений на операторную норму.

LaTeX

$$$f:\\;E\\to_L F\\;\\Rightarrow\\; f\\text{ HasTemperateGrowth}$.$$

Lean4

theorem _root_.ContinuousLinearMap.hasTemperateGrowth (f : E →L[ℝ] F) : Function.HasTemperateGrowth f :=
  by
  apply Function.HasTemperateGrowth.of_fderiv ?_ f.differentiable (k := 1) (C := ‖f‖) (fun x ↦ ?_)
  · have : fderiv ℝ f = fun _ ↦ f := by ext1 v; simp only [ContinuousLinearMap.fderiv]
    simpa [this] using .const _
  · exact (f.le_opNorm x).trans (by simp [mul_add])

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