Gaussian bounds for the heat kernel and its derivatives

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)) is controlled by the heat kernel at a later time: trading time for decay absorbs polynomial weights and translations. This file records the bounds used to differentiate heat convolutions under the integral sign:

• the comparison K_s ≤ (s' / s)^(n/2) K_{s'} for 0 < s ≤ s';
• translations: K_t(z + h) ≤ 2^(n/2) exp(‖h‖² / (4t)) K_{2t}(z);
• polynomial weights: (1 + ‖x‖)^m K_t(x) ≤ C K_{2t}(x) for some C > 0, and, for α ≥ 0, ‖x‖^α K_t(x) ≤ C t^(α / 2) K_{2t}(x) with C independent of t > 0;
• derivatives of every order, against every polynomial weight: (1 + ‖x‖)^p ‖D^k K_t(x)‖ ≤ C K_{2t}(x) for some C > 0, so that each derivative is integrable and is dominated, uniformly on translates of any bounded radius, by an integrable function.

The derivative bound comes from Mathlib's Faà di Bruno estimate norm_iteratedFDeriv_comp_le for exp ∘ (-‖·‖² / (4t)), together with the temperate growth of ‖·‖².

Main declarations

• TauCeti.heatKernel_le_mul_heatKernel: comparison of heat kernels at two times.
• TauCeti.heatKernel_eq_mul_heatKernel_two_mul: K_t = 2^(n/2) exp(-‖x‖² / (8t)) K_{2t}.
• TauCeti.heatKernel_add_le: the translation bound.
• TauCeti.exists_one_add_norm_pow_mul_heatKernel_le: polynomial weights.
• TauCeti.exists_norm_rpow_mul_heatKernel_le: absorbing the weight ‖x‖^α into K_{2t}, with a constant independent of the time.
• TauCeti.exists_one_add_norm_pow_mul_norm_iteratedFDeriv_heatKernel_le and TauCeti.exists_norm_iteratedFDeriv_heatKernel_le: Gaussian bounds on all derivatives, with and without polynomial weights.
• TauCeti.exists_integrable_norm_iteratedFDeriv_heatKernel_add_le: integrable domination of the derivatives on translates of any bounded radius.
• TauCeti.integrable_iteratedFDeriv_heatKernel: every derivative is integrable.

theorem TauCeti.heatKernel_le_mul_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s s' : ℝ} (hs : 0 < s) (hss' : s ≤ s') (x : E) : heatKernel s x ≤ (s' / s) ^ (↑(Module.finrank ℝ E) / 2) * heatKernel s' x

Comparison of heat kernels. For 0 < s ≤ s', K_s ≤ (s' / s)^(n/2) K_{s'}.

theorem TauCeti.heatKernel_eq_mul_heatKernel_two_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (x : E) : heatKernel t x = 2 ^ (↑(Module.finrank ℝ E) / 2) * Real.exp (-‖x‖ ^ 2 / (8 * t)) * heatKernel (2 * t) x

The heat kernel at time t is the heat kernel at time 2t times a Gaussian factor: K_t(x) = 2^(n/2) exp(-‖x‖² / (8t)) K_{2t}(x).

theorem TauCeti.heatKernel_add_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (z h : E) : heatKernel t (z + h) ≤ 2 ^ (↑(Module.finrank ℝ E) / 2) * Real.exp (‖h‖ ^ 2 / (4 * t)) * heatKernel (2 * t) z

Translating the heat kernel. K_t(z + h) ≤ 2^(n/2) exp(‖h‖² / (4t)) K_{2t}(z): a translate of the heat kernel is dominated by the heat kernel at twice the time.

theorem TauCeti.exists_one_add_norm_pow_mul_heatKernel_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (m : ℕ) : ∃ C > 0, ∀ (x : E), (1 + ‖x‖) ^ m * heatKernel t x ≤ C * heatKernel (2 * t) x

Polynomial weights. For every m, (1 + ‖x‖)^m K_t(x) ≤ C K_{2t}(x) for some positive C.

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

Scale-invariant polynomial weights. For α ≥ 0 there is a constant C > 0, independent of the time, with ‖x‖^α K_t(x) ≤ C t^(α/2) K_{2t}(x) for all t > 0 and all x.

theorem TauCeti.exists_one_add_norm_pow_mul_norm_iteratedFDeriv_heatKernel_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (k p : ℕ) : ∃ C > 0, ∀ (x : E), (1 + ‖x‖) ^ p * ‖iteratedFDeriv ℝ k (heatKernel t) x‖ ≤ C * heatKernel (2 * t) x

Weighted Gaussian bounds on the derivatives of the heat kernel. For every order k and every weight exponent p there is a positive constant C with (1 + ‖x‖)^p ‖D^k K_t(x)‖ ≤ C K_{2t}(x) for all x.

theorem TauCeti.exists_norm_iteratedFDeriv_heatKernel_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (k : ℕ) : ∃ C > 0, ∀ (x : E), ‖iteratedFDeriv ℝ k (heatKernel t) x‖ ≤ C * heatKernel (2 * t) x

Gaussian bounds on the derivatives of the heat kernel. For every order k there is a positive constant C with ‖D^k K_t(x)‖ ≤ C K_{2t}(x) for all x.

theorem TauCeti.exists_integrable_norm_iteratedFDeriv_heatKernel_add_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {t : ℝ} (ht : 0 < t) (k : ℕ) (R : ℝ) : ∃ (w : E → ℝ), MeasureTheory.Integrable w MeasureTheory.volume ∧ ∀ (z h : E), ‖h‖ ≤ R → ‖iteratedFDeriv ℝ k (heatKernel t) (z + h)‖ ≤ w z

Every derivative of the heat kernel is dominated, uniformly on translates of norm at most R, by an integrable function (a multiple of K_{4t}).

theorem TauCeti.integrable_iteratedFDeriv_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {t : ℝ} (ht : 0 < t) (m : ℕ) : MeasureTheory.Integrable (iteratedFDeriv ℝ m (heatKernel t)) MeasureTheory.volume

Every derivative of the heat kernel is integrable.