Derivatives of functions of temperate growth

A smooth function whose iterated derivatives are all bounded has temperate growth. Typical examples are smooth functions which outside a ball agree with a homogeneous function of degree at most 0. So does a smooth function satisfying symbol estimates ‖D^k f(x)‖ ≤ C_k (1 + ‖x‖ ^ 2) ^ ((m - k) / 2) of some real order m, and the rescaled Bessel potential x ↦ (1 + ‖c • x‖ ^ 2) ^ r.

The derivative Df of a function f of temperate growth has temperate growth, since the iterated derivatives of Df are those of f shifted by one order. So does each directional derivative x ↦ Df(x) v. These are the coefficients that appear when the Leibniz rule is applied to the product of a Schwartz function or a tempered distribution with f.

A measure of temperate growth is finite on compact sets.

Main results

• Function.HasTemperateGrowth.of_norm_iteratedFDeriv_le: bounded derivatives give temperate growth.
• Function.HasTemperateGrowth.of_norm_iteratedFDeriv_le_one_add_norm_sq_rpow: symbol estimates give temperate growth.
• Function.hasTemperateGrowth_one_add_norm_smul_sq_rpow: the rescaled Bessel potential has temperate growth.
• Function.hasTemperateGrowth_norm_sub_pow: y ↦ ‖x - y‖ ^ (2N) has temperate growth.
• Function.HasTemperateGrowth.fderiv: Df has temperate growth.
• Function.HasTemperateGrowth.fderiv_apply: x ↦ Df(x) v has temperate growth.
• MeasureTheory.Measure.HasTemperateGrowth.isFiniteMeasureOnCompacts: a measure of temperate growth is finite on compact sets.

theorem Function.HasTemperateGrowth.of_norm_iteratedFDeriv_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (hbd : ∀ (n : ℕ), ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C) : HasTemperateGrowth f

A smooth function all of whose iterated derivatives are bounded has temperate growth.

theorem Function.HasTemperateGrowth.of_norm_iteratedFDeriv_le_one_add_norm_sq_rpow {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {m : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hbound : ∀ (k : ℕ), ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ k f x‖ ≤ C * (1 + ‖x‖ ^ 2) ^ ((m - ↑k) / 2)) : HasTemperateGrowth f

Symbol estimates give temperate growth. A smooth function whose k-th derivative is bounded by C_k (1 + ‖x‖²) ^ ((m - k) / 2) for every k has temperate growth.

theorem Function.HasTemperateGrowth.fderiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf : HasTemperateGrowth f) : HasTemperateGrowth (_root_.fderiv ℝ f)

The derivative of a function of temperate growth has temperate growth.

theorem Function.HasTemperateGrowth.fderiv_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf : HasTemperateGrowth f) (v : E) : HasTemperateGrowth fun (x : E) => (_root_.fderiv ℝ f x) v

A directional derivative x ↦ Df(x) v of a function of temperate growth has temperate growth.

theorem Function.hasTemperateGrowth_one_add_norm_smul_sq_rpow {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (c r : ℝ) : HasTemperateGrowth fun (x : H) => (1 + ‖c • x‖ ^ 2) ^ r

The rescaled Bessel potential x ↦ (1 + ‖c • x‖ ^ 2) ^ r has temperate growth.

theorem Function.hasTemperateGrowth_norm_sub_pow {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (x : H) (N : ℕ) : HasTemperateGrowth fun (y : H) => ‖x - y‖ ^ (2 * N)

An even power y ↦ ‖x - y‖ ^ (2N) of the distance to a point has temperate growth.

theorem MeasureTheory.Measure.HasTemperateGrowth.isFiniteMeasureOnCompacts {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] (μ : Measure E) [h : μ.HasTemperateGrowth] : IsFiniteMeasureOnCompacts μ

A measure of temperate growth is finite on compact sets: (1 + ‖x‖) ^ (-n) is integrable and bounded below by a positive constant on any bounded set.