Heat Convolution #
A smooth compactly supported input has a smooth Gaussian heat orbit at every positive time.
theorem
ESS.heatConv_smooth_input
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hfc : HasCompactSupport f)
{t : ℝ}
(ht : 0 < t)
:
ContDiff ℝ (↑⊤) (CKN.Foundation.Heat.heatConv t f)
A smooth compactly supported input has a smooth Gaussian heat orbit at every positive time.
theorem
ESS.heatConv_abs_le_spatial_decay
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hfc : HasCompactSupport f)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ {t : ℝ},
0 < t →
∀ (x : CKN.Foundation.Parabolic.Vec3),
|CKN.Foundation.Heat.heatConv t f x| ≤ C / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 3
Smooth compact data have a uniform polynomial tail under positive-time heat
convolution. This is used to justify the whole-space entropy test in
lem:pv-heat-critical.
theorem
ESS.heatConv_memLp_two_smooth
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hfc : HasCompactSupport f)
{t : ℝ}
(ht : 0 < t)
:
Positive-time heat evolution of smooth compact data belongs to spatial
L²; the tail estimate is uniform up to time zero.
theorem
ESS.heatConv_fderiv
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hfc : HasCompactSupport f)
{t : ℝ}
(ht : 0 < t)
(x v : CKN.Foundation.Parabolic.Vec3)
:
(fderiv ℝ (CKN.Foundation.Heat.heatConv t f) x) v = CKN.Foundation.Heat.heatConv t (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ f y) v) x
A spatial derivative of a Gaussian heat orbit is the heat orbit of the corresponding derivative of smooth compactly supported data.