Scale-invariant bounds on the space-time derivatives of the heat kernel

On a finite-dimensional real inner product space E of dimension n, the heat kernel K_t(x) = (4πt)^(-n/2) exp(-‖x‖² / (4t)) has the parabolic scaling D^m K_t(x) = t^(-(n + m) / 2) D^m K_1(t^(-1/2) x). This file turns that scaling into estimates whose constants do not depend on the time, as needed for the Hölder estimates of heat potentials:

• for all orders j in time and m in space, ‖∂ₜ^j D^m K_t(x)‖ ≤ C t^(-(n + m + 2j) / 2) exp(-‖x‖² / (8t)) for all t > 0;
• equivalently for j = 0, ‖D^m K_t(x)‖ ≤ C t^(-m / 2) K_{2t}(x);
• rescaling the case t = 1 / 4, the derivatives of the Gaussian exp(-c ‖x‖²) satisfy ‖D^m exp(-c ‖x‖²)‖ ≤ C c^(m / 2) exp(-c ‖x‖² / 2) uniformly in c ≥ 0;
• ‖D^m K_t(x)‖ ‖x‖^α ≤ C t^((α - m) / 2) K_{4t}(x) for α ≥ 0;
• consequently ∫ ‖D^m K_t(x)‖ ‖x‖^α dx ≤ C t^((α - m) / 2), in particular ∫ ‖D^m K_t‖ ≤ C t^(-m / 2);
• for time differences, ∫ ‖D^m K_b(x) - D^m K_a(x)‖ ‖x‖^α dx ≤ C (b - a) a^((α - m - 2) / 2) when 0 < a ≤ b ≤ 2a, by the mean value theorem in time;
• ∫ D^m K_t = 0 for m ≥ 1.

Every time derivative of D^m K_s(x) at s = t again has the scaling form s^(-b) Ψ(s^(-1/2) x) for a profile Ψ all of whose derivatives decay like exp(-‖y‖² / 8), so the time bound reduces to a bound on the profile. The vanishing integral follows by integrating by parts against the constant function 1.

Main declarations

• TauCeti.iteratedFDeriv_heatKernel_eq_rpow_smul: parabolic scaling of the derivatives.
• TauCeti.differentiableAt_iteratedFDeriv_heatKernel: the spatial derivatives are differentiable in time.
• TauCeti.exists_norm_iteratedDeriv_iteratedFDeriv_heatKernel_le: Gaussian bounds on the space-time derivatives.
• TauCeti.exists_norm_iteratedFDeriv_heatKernel_le_rpow_mul_exp: the case of spatial derivatives.
• TauCeti.exists_norm_iteratedFDeriv_exp_neg_mul_norm_sq_le: the derivatives of the Gaussian exp(-c ‖ξ‖²) are O(c^{k/2} exp(-c ‖ξ‖² / 2)), uniformly in c ≥ 0.
• TauCeti.exists_norm_iteratedFDeriv_heatKernel_le_mul_rpow_mul_heatKernel: the bound by C t^(-m / 2) K_{2t}(x).
• TauCeti.exists_norm_iteratedFDeriv_heatKernel_mul_rpow_le: the weighted bound by C t^((α - m) / 2) K_{4t}(x).
• TauCeti.integrable_norm_iteratedFDeriv_heatKernel_mul_rpow: integrability of the weighted derivatives.
• TauCeti.integrable_norm_rpow_mul_heatKernel: integrability of the weight ‖x‖^α K_t(x).
• TauCeti.heatKernelMoment: the absolute moment ∫ ‖y‖^α K_1(y) dy.
• TauCeti.exists_integral_norm_iteratedFDeriv_heatKernel_mul_rpow_le: the weighted L¹ bound.
• TauCeti.exists_integral_norm_iteratedFDeriv_heatKernel_le: the L¹ bound.
• TauCeti.exists_norm_iteratedFDeriv_heatKernel_sub_mul_rpow_le, TauCeti.exists_integral_norm_iteratedFDeriv_heatKernel_sub_mul_rpow_le: the weighted bounds on time differences.
• TauCeti.integral_iteratedFDeriv_heatKernel_eq_zero: the derivatives have integral zero.

References

• A. Friedman, Partial Differential Equations of Parabolic Type, Chapter 1 (Gaussian bounds on the derivatives of the fundamental solution).
• A. Lunardi, Linear and nonlinear diffusion problems, Chapter 4 (weighted kernel estimates for heat potentials).

theorem TauCeti.iteratedFDeriv_heatKernel_eq_rpow_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (m : ℕ) (x : E) : iteratedFDeriv ℝ m (heatKernel t) x = t ^ (-(↑(Module.finrank ℝ E) + ↑m) / 2) • iteratedFDeriv ℝ m (heatKernel 1) (t ^ (-1 / 2) • x)

Parabolic scaling of the derivatives of the heat kernel. For t > 0, D^m K_t(x) = t^(-(n + m) / 2) D^m K_1(t^(-1/2) x), where n = dim E.

Time derivatives

By parabolic scaling, D^m K_s(x) = s^(-a) Ψ(s^(-1/2) x) with a = (n + m) / 2 and Ψ = D^m K_1. Differentiating such an expression in s gives one of the same shape, s^(-(a + 1)) Ψ'(s^(-1/2) x) with Ψ'(y) = -a Ψ(y) - (1/2) DΨ(y) y. Since Ψ has Gaussian decay at rate 1 / 8 and that class is closed under Ψ ↦ Ψ' (exists_gaussianDecay_iteratedDeriv_rpow_smul), every time derivative has a Gaussian bound.

theorem TauCeti.exists_norm_iteratedDeriv_iteratedFDeriv_heatKernel_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (j m : ℕ) : ∃ (C : ℝ), ∀ (t : ℝ), 0 < t → ∀ (x : E), ‖iteratedDeriv j (fun (s : ℝ) => iteratedFDeriv ℝ m (heatKernel s) x) t‖ ≤ C * t ^ (-(↑(Module.finrank ℝ E) + ↑m + 2 * ↑j) / 2) * Real.exp (-‖x‖ ^ 2 / (8 * t))

Gaussian bounds on the space-time derivatives of the heat kernel. For all orders j in time and m in space there is a constant C, independent of the time, such that ‖∂ₜ^j D^m K_t(x)‖ ≤ C t^(-(n + m + 2j) / 2) exp(-‖x‖² / (8t)) for all t > 0 and all x, where n = dim E.

theorem TauCeti.differentiableAt_iteratedFDeriv_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (m : ℕ) (x : E) : DifferentiableAt ℝ (fun (s : ℝ) => iteratedFDeriv ℝ m (heatKernel s) x) t

For t > 0, the spatial derivative D^m K_s(x) of the heat kernel is differentiable in the time s at s = t.

theorem TauCeti.exists_norm_iteratedFDeriv_heatKernel_le_rpow_mul_exp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : ℕ) : ∃ (C : ℝ), ∀ (t : ℝ), 0 < t → ∀ (x : E), ‖iteratedFDeriv ℝ m (heatKernel t) x‖ ≤ C * t ^ (-(↑(Module.finrank ℝ E) + ↑m) / 2) * Real.exp (-‖x‖ ^ 2 / (8 * t))

Scale-invariant Gaussian bounds on the derivatives of the heat kernel. For every order m there is a constant C, independent of the time, such that ‖D^m K_t(x)‖ ≤ C t^(-(n + m) / 2) exp(-‖x‖² / (8t)) for all t > 0 and all x, where n = dim E.

theorem TauCeti.exists_norm_iteratedFDeriv_exp_neg_mul_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (k : ℕ) : ∃ (C : ℝ), ∀ (c : ℝ), 0 ≤ c → ∀ (ξ : E), ‖iteratedFDeriv ℝ k (fun (ξ : E) => Real.exp (-(c * ‖ξ‖ ^ 2))) ξ‖ ≤ C * √c ^ k * Real.exp (-(c * ‖ξ‖ ^ 2) / 2)

Derivatives of a Gaussian. For every order k there is a constant C such that, for every c ≥ 0, ‖D^k exp(-c ‖ξ‖²)‖ ≤ C c^{k/2} exp(-c ‖ξ‖² / 2).

theorem TauCeti.exists_norm_iteratedFDeriv_heatKernel_le_mul_rpow_mul_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : ℕ) : ∃ C > 0, ∀ (t : ℝ), 0 < t → ∀ (x : E), ‖iteratedFDeriv ℝ m (heatKernel t) x‖ ≤ C * t ^ (-↑m / 2) * heatKernel (2 * t) x

Scale-invariant Gaussian bounds on the derivatives of the heat kernel, against the heat kernel at the doubled time. For every order m there is a constant C > 0, independent of the time, such that ‖D^m K_t(x)‖ ≤ C t^(-m / 2) K_{2t}(x) for all t > 0 and all x.

theorem TauCeti.exists_norm_iteratedFDeriv_heatKernel_mul_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : ℕ) {α : ℝ} (hα : 0 ≤ α) : ∃ C > 0, ∀ (t : ℝ), 0 < t → ∀ (x : E), ‖iteratedFDeriv ℝ m (heatKernel t) x‖ * ‖x‖ ^ α ≤ C * t ^ ((α - ↑m) / 2) * heatKernel (4 * t) x

Scale-invariant weighted Gaussian bounds on the derivatives of the heat kernel. For every order m and every α ≥ 0 there is a constant C > 0, independent of the time, with ‖D^m K_t(x)‖ ‖x‖^α ≤ C t^((α - m)/2) K_{4t}(x) for all t > 0 and all x.

theorem TauCeti.exists_norm_iteratedFDeriv_heatKernel_sub_mul_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : ℕ) {α : ℝ} (hα : 0 ≤ α) : ∃ C > 0, ∀ (a b : ℝ), 0 < a → a ≤ b → b ≤ 2 * a → ∀ (x : E), ‖iteratedFDeriv ℝ m (heatKernel b) x - iteratedFDeriv ℝ m (heatKernel a) x‖ * ‖x‖ ^ α ≤ C * (b - a) * a ^ ((α - ↑m - 2) / 2) * heatKernel (4 * b) x

Time differences of the derivatives of the heat kernel. For every order m and every α ≥ 0 there is a constant C > 0, independent of the times, such that ‖D^m K_b(x) - D^m K_a(x)‖ ‖x‖^α ≤ C (b - a) a^((α - m - 2)/2) K_{4b}(x) whenever 0 < a ≤ b ≤ 2a. One time derivative costs a factor a⁻¹ compared with TauCeti.exists_norm_iteratedFDeriv_heatKernel_mul_rpow_le.

theorem TauCeti.integrable_norm_iteratedFDeriv_heatKernel_mul_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {t : ℝ} (ht : 0 < t) (m : ℕ) {α : ℝ} (hα : 0 ≤ α) : MeasureTheory.Integrable (fun (x : E) => ‖iteratedFDeriv ℝ m (heatKernel t) x‖ * ‖x‖ ^ α) MeasureTheory.volume

For t > 0 and α ≥ 0, the weighted derivative x ↦ ‖D^m K_t(x)‖ ‖x‖^α of the heat kernel is integrable.

theorem TauCeti.integrable_norm_rpow_mul_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {t : ℝ} (ht : 0 < t) {α : ℝ} (hα : 0 ≤ α) : MeasureTheory.Integrable (fun (x : E) => ‖x‖ ^ α * heatKernel t x) MeasureTheory.volume

For t > 0 and α ≥ 0, the weight x ↦ ‖x‖^α K_t(x) is integrable.

noncomputable def TauCeti.heatKernelMoment (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (α : NNReal) : NNReal

The absolute moment M_α = ∫ ‖y‖^α K_1(y) dy of order α of the heat kernel at time one. It is the constant in the Hölder estimates of heat potentials.

theorem TauCeti.coe_heatKernelMoment {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (α : NNReal) : ↑(heatKernelMoment E α) = ∫ (y : E), ‖y‖ ^ ↑α * heatKernel 1 y

The defining formula of TauCeti.heatKernelMoment.

theorem TauCeti.exists_integral_norm_iteratedFDeriv_heatKernel_mul_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (m : ℕ) {α : ℝ} (hα : 0 ≤ α) : ∃ C > 0, ∀ (t : ℝ), 0 < t → ∫ (x : E), ‖iteratedFDeriv ℝ m (heatKernel t) x‖ * ‖x‖ ^ α ≤ C * t ^ ((α - ↑m) / 2)

Weighted L¹ bounds on the derivatives of the heat kernel. For every order m and every α ≥ 0 there is a constant C > 0, independent of the time, with ∫ ‖D^m K_t(x)‖ ‖x‖^α dx ≤ C t^((α - m)/2) for all t > 0. Combined with the cancellation ∫ D^m K_t = 0, this is the kernel estimate behind Hölder bounds for heat convolutions.

theorem TauCeti.exists_integral_norm_iteratedFDeriv_heatKernel_sub_mul_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (m : ℕ) {α : ℝ} (hα : 0 ≤ α) : ∃ C > 0, ∀ (a b : ℝ), 0 < a → a ≤ b → b ≤ 2 * a → ∫ (x : E), ‖iteratedFDeriv ℝ m (heatKernel b) x - iteratedFDeriv ℝ m (heatKernel a) x‖ * ‖x‖ ^ α ≤ C * (b - a) * a ^ ((α - ↑m - 2) / 2)

Weighted L¹ bounds on time differences of the derivatives of the heat kernel. For every order m and every α ≥ 0 there is a constant C > 0, independent of the times, with ∫ ‖D^m K_b(x) - D^m K_a(x)‖ ‖x‖^α dx ≤ C (b - a) a^((α - m - 2)/2) whenever 0 < a ≤ b ≤ 2a. This is the kernel estimate behind temporal Hölder bounds for heat convolutions.

theorem TauCeti.exists_integral_norm_iteratedFDeriv_heatKernel_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (m : ℕ) : ∃ (C : ℝ), ∀ (t : ℝ), 0 < t → ∫ (x : E), ‖iteratedFDeriv ℝ m (heatKernel t) x‖ ≤ C * t ^ (-↑m / 2)

Scale-invariant L¹ bounds on the derivatives of the heat kernel. For every order m there is a constant C, independent of the time, such that ‖D^m K_t‖_{L¹} ≤ C t^(-m / 2) for all t > 0.

@[simp]

theorem TauCeti.integral_iteratedFDeriv_heatKernel_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {t : ℝ} (ht : 0 < t) {m : ℕ} (hm : m ≠ 0) : ∫ (x : E), iteratedFDeriv ℝ m (heatKernel t) x = 0

The derivatives of the heat kernel have integral zero. For every order m ≥ 1 and every t > 0, ∫ D^m K_t = 0.