Functions and measures of temperate growth

def Function.HasTemperateGrowth {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) : Prop

A function is called of temperate growth if it is smooth and all iterated derivatives are polynomially bounded.

Equations

• Function.HasTemperateGrowth f = (ContDiff ℝ (↑⊤) f ∧ ∀ (n : ℕ), ∃ (k : ℕ) (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C * (1 + ‖x‖) ^ k)

theorem Function.hasTemperateGrowth_iff_isBigO {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} : HasTemperateGrowth f ↔ ContDiff ℝ (↑⊤) f ∧ ∀ (n : ℕ), ∃ (k : ℕ), iteratedFDeriv ℝ n f =O[⊤] fun (x : E) => (1 + ‖x‖) ^ k

A function has temperate growth if and only if it is smooth and its n-th iterated derivative is O((1 + ‖x‖) ^ k) for some k : ℕ (depending on n).

Note that the O here is with respect to the ⊤ filter, meaning that the bound holds everywhere.

TODO: when E is finite dimensional, this is equivalent to the derivatives being O(‖x‖ ^ k) as ‖x‖ → ∞.

theorem Function.HasTemperateGrowth.isBigO {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf_temperate : HasTemperateGrowth f) (n : ℕ) : ∃ (k : ℕ), iteratedFDeriv ℝ n f =O[⊤] fun (x : E) => (1 + ‖x‖) ^ k

If f has temperate growth, then its n-th iterated derivative is O((1 + ‖x‖) ^ k) for some k : ℕ (depending on n).

Note that the O here is with respect to the ⊤ filter, meaning that the bound holds everywhere.

theorem Function.HasTemperateGrowth.isBigO_uniform {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf_temperate : HasTemperateGrowth f) (N : ℕ) : ∃ (k : ℕ), ∀ n ≤ N, iteratedFDeriv ℝ n f =O[⊤] fun (x : E) => (1 + ‖x‖) ^ k

If f has temperate growth, then for any N : ℕ one can find k such that all iterated derivatives of f of order ≤ N are O((1 + ‖x‖) ^ k).

Note that the O here is with respect to the ⊤ filter, meaning that the bound holds everywhere.

theorem Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf_temperate : HasTemperateGrowth f) (n : ℕ) : ∃ (k : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k

@[deprecated Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform (since := "2025-10-30")]

theorem Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf_temperate : HasTemperateGrowth f) (n : ℕ) : ∃ (k : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k

Alias of Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform.

theorem Function.HasTemperateGrowth.of_fderiv {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (h'f : HasTemperateGrowth (fderiv ℝ f)) (hf : Differentiable ℝ f) {k : ℕ} {C : ℝ} (h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k) : HasTemperateGrowth f

theorem Function.HasTemperateGrowth.zero {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : HasTemperateGrowth fun (x : E) => 0

theorem Function.HasTemperateGrowth.const {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : F) : HasTemperateGrowth fun (x : E) => c

theorem Function.HasTemperateGrowth.comp' {D : Type u_3} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup D] [NormedSpace ℝ D] {g : E → F} {f : D → E} {t : Set E} (ht : Set.range f ⊆ t) (ht' : UniqueDiffOn ℝ t) (hg₁ : ContDiffOn ℝ (↑⊤) g t) (hg₂ : ∀ (N : ℕ), ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k) (hf : HasTemperateGrowth f) : HasTemperateGrowth (g ∘ f)

Composition of two temperate growth functions is of temperate growth.

Version where the outer function g is only of temperate growth on the image of inner function f.

theorem Function.HasTemperateGrowth.comp {D : Type u_3} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup D] [NormedSpace ℝ D] {g : E → F} {f : D → E} (hg : HasTemperateGrowth g) (hf : HasTemperateGrowth f) : HasTemperateGrowth (g ∘ f)

Composition of two temperate growth functions is of temperate growth.

theorem Function.HasTemperateGrowth.neg {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf : HasTemperateGrowth f) : HasTemperateGrowth (-f)

theorem Function.HasTemperateGrowth.add {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : E → F} (hf : HasTemperateGrowth f) (hg : HasTemperateGrowth g) : HasTemperateGrowth (f + g)

theorem Function.HasTemperateGrowth.sub {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : E → F} (hf : HasTemperateGrowth f) (hg : HasTemperateGrowth g) : HasTemperateGrowth (f - g)

theorem ContinuousLinearMap.bilinear_hasTemperateGrowth {𝕜 : Type u_1} {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 G] [NormedSpace 𝕜 E] (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F} (hf : Function.HasTemperateGrowth f) (hg : Function.HasTemperateGrowth g) : Function.HasTemperateGrowth fun (x : D) => (B (f x)) (g x)

The product of two functions of temperate growth is again of temperate growth.

Version for bilinear maps.

theorem Function.HasTemperateGrowth.id {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] : HasTemperateGrowth _root_.id

theorem Function.HasTemperateGrowth.id' {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] : HasTemperateGrowth fun (x : E) => x

theorem Function.HasTemperateGrowth.smul {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] {f : E → 𝕜} {g : E → F} (hf : HasTemperateGrowth f) (hg : HasTemperateGrowth g) : HasTemperateGrowth (f • g)

The product of two functions of temperate growth is again of temperate growth.

Version for scalar multiplication.

theorem Function.HasTemperateGrowth.mul {R : Type u_2} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedRing R] [NormedAlgebra ℝ R] {f g : E → R} (hf : HasTemperateGrowth f) (hg : HasTemperateGrowth g) : HasTemperateGrowth (f * g)

The product of two functions of temperate growth is again of temperate growth.

theorem Function.HasTemperateGrowth.pow {R : Type u_2} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedRing R] [NormedAlgebra ℝ R] {f : E → R} (hf : HasTemperateGrowth f) (k : ℕ) : HasTemperateGrowth (f ^ k)

theorem ContinuousLinearMap.hasTemperateGrowth {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E →L[ℝ] F) : Function.HasTemperateGrowth ⇑f

theorem Function.hasTemperateGrowth_norm_sq (H : Type u_7) [NormedAddCommGroup H] [InnerProductSpace ℝ H] : HasTemperateGrowth fun (x : H) => ‖x‖ ^ 2

class MeasureTheory.Measure.HasTemperateGrowth {E : Type u_4} [NormedAddCommGroup E] [MeasurableSpace E] (μ : Measure E) : Prop

A measure μ has temperate growth if there is an n : ℕ such that (1 + ‖x‖) ^ (- n) is μ-integrable.

• exists_integrable : ∃ (n : ℕ), Integrable (fun (x : E) => (1 + ‖x‖) ^ (-↑n)) μ

def MeasureTheory.Measure.integrablePower {E : Type u_4} [NormedAddCommGroup E] [MeasurableSpace E] (μ : Measure E) : ℕ

An integer exponent l such that (1 + ‖x‖) ^ (-l) is integrable if μ has temperate growth.

Equations

• μ.integrablePower = if h : μ.HasTemperateGrowth then ⋯.choose else 0

theorem MeasureTheory.Measure.integrable_pow_neg_integrablePower {E : Type u_4} [NormedAddCommGroup E] [MeasurableSpace E] (μ : Measure E) [h : μ.HasTemperateGrowth] : Integrable (fun (x : E) => (1 + ‖x‖) ^ (-↑μ.integrablePower)) μ

instance MeasureTheory.IsFiniteMeasure.instHasTemperateGrowth {E : Type u_4} [NormedAddCommGroup E] [MeasurableSpace E] {μ : Measure E} [h : IsFiniteMeasure μ] : μ.HasTemperateGrowth

instance MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth {E : Type u_4} [NormedAddCommGroup E] [MeasurableSpace E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : Measure E} [h : μ.IsAddHaarMeasure] : μ.HasTemperateGrowth

theorem pow_mul_le_of_le_of_pow_mul_le {C₁ C₂ : ℝ} {k l : ℕ} {x f : ℝ} (hx : 0 ≤ x) (hf : 0 ≤ f) (h₁ : f ≤ C₁) (h₂ : x ^ (k + l) * f ≤ C₂) : x ^ k * f ≤ 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l)

Pointwise inequality to control x ^ k * f in terms of 1 / (1 + x) ^ l if one controls both f (with a bound C₁) and x ^ (k + l) * f (with a bound C₂). This will be used to check integrability of x ^ k * f x when f is a Schwartz function, and to control explicitly its integral in terms of suitable seminorms of f.

theorem integrable_of_le_of_pow_mul_le {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [MeasurableSpace E] [NormedAddCommGroup F] [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} [μ.HasTemperateGrowth] {f : E → F} {C₁ C₂ : ℝ} {k : ℕ} (hf : ∀ (x : E), ‖f x‖ ≤ C₁) (h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂) (h''f : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.Integrable (fun (x : E) => ‖x‖ ^ k * ‖f x‖) μ

Given a function such that f and x ^ (k + l) * f are bounded for a suitable l, then x ^ k * f is integrable. The bounds are not relevant for the integrability conclusion, but they are relevant for bounding the integral in integral_pow_mul_le_of_le_of_pow_mul_le. We formulate the two lemmas with the same set of assumptions for ease of applications.

theorem integral_pow_mul_le_of_le_of_pow_mul_le {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [MeasurableSpace E] [NormedAddCommGroup F] {μ : MeasureTheory.Measure E} [μ.HasTemperateGrowth] {f : E → F} {C₁ C₂ : ℝ} {k : ℕ} (hf : ∀ (x : E), ‖f x‖ ≤ C₁) (h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂) : ∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ (2 ^ μ.integrablePower * ∫ (x : E), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) * (C₁ + C₂)

Given a function such that f and x ^ (k + l) * f are bounded for a suitable l, then one can bound explicitly the integral of x ^ k * f.

theorem MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top {E : Type u_4} [NormedAddCommGroup E] [MeasurableSpace E] (p : ENNReal) {μ : Measure E} (hμ : μ.HasTemperateGrowth) : ∃ (k : ℕ), eLpNorm (fun (x : E) => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤

For any HasTemperateGrowth measure and p, there exists an integer power k such that (1 + ‖x‖) ^ (-k) is in L^p.