Functions with Gaussian decay

A function Ψ : E → F has Gaussian decay at rate c if it is smooth and each of its iterated derivatives, against every polynomial weight (1 + ‖y‖)^p, is dominated by exp(-c ‖y‖²). This class is closed under scalar multiplication, subtraction and Ψ ↦ (y ↦ DΨ(y) y).

Consequently it is stable under the time derivatives of parabolically rescaled profiles: every iterated derivative in s of s^(-a) Ψ(s^(-1/2) x) is again of the form s^(-(a + j)) Φ(s^(-1/2) x) with Φ of Gaussian decay at the same rate. This is how the time derivatives of the heat kernel are bounded.

Main declarations

• TauCeti.GaussianDecay: smoothness with Gaussian decay of all weighted derivatives.
• TauCeti.exists_gaussianDecay_iteratedDeriv_rpow_smul: iterated time derivatives of parabolically rescaled profiles with Gaussian decay.

structure TauCeti.GaussianDecay {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (Ψ : E → F) : Prop

Ψ has Gaussian decay at rate c: it is smooth, and each of its iterated derivatives, against every polynomial weight (1 + ‖y‖)^p, is dominated by the Gaussian exp(-c ‖y‖²).

• contDiff : ContDiff ℝ (↑⊤) Ψ

  A function with Gaussian decay is smooth.

• exists_bound (i p : ℕ) : ∃ (C : ℝ), ∀ (y : E), (1 + ‖y‖) ^ p * ‖iteratedFDeriv ℝ i Ψ y‖ ≤ C * Real.exp (-c * ‖y‖ ^ 2)

  Every weighted iterated derivative is dominated by the Gaussian.

theorem TauCeti.GaussianDecay.const_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} {Ψ : E → F} (hΨ : GaussianDecay c Ψ) (a : ℝ) : GaussianDecay c fun (y : E) => a • Ψ y

Gaussian decay is preserved by scalar multiplication.

theorem TauCeti.GaussianDecay.sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} {Ψ Φ : E → F} (hΨ : GaussianDecay c Ψ) (hΦ : GaussianDecay c Φ) : GaussianDecay c fun (y : E) => Ψ y - Φ y

Gaussian decay is preserved by subtraction.

theorem TauCeti.GaussianDecay.fderiv_apply_self {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} {Ψ : E → F} (hΨ : GaussianDecay c Ψ) : GaussianDecay c fun (y : E) => (fderiv ℝ Ψ y) y

If Ψ has Gaussian decay, so does y ↦ DΨ(y) y: the polynomial weights absorb the factor y.

theorem TauCeti.exists_gaussianDecay_iteratedDeriv_rpow_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (j : ℕ) (a : ℝ) {Ψ : E → F} : GaussianDecay c Ψ → ∃ (Φ : E → F), GaussianDecay c Φ ∧ ∀ (x : E) (s : ℝ), 0 < s → iteratedDeriv j (fun (s : ℝ) => s ^ (-a) • Ψ (s ^ (-1 / 2) • x)) s = s ^ (-(a + ↑j)) • Φ (s ^ (-1 / 2) • x)

Iterated time derivatives of a parabolically rescaled profile with Gaussian decay are again rescaled profiles with Gaussian decay at the same rate.