Heat PDE #
A smooth compact input evolves by the heat equation under Gaussian convolution.
theorem
ESS.heatConv_hasDerivAt_laplacianInput
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hfc : HasCompactSupport f)
{t : ℝ}
(ht : 0 < t)
(x : CKN.Foundation.Parabolic.Vec3)
:
HasDerivAt (fun (s : ℝ) => CKN.Foundation.Heat.heatConv s f x)
(CKN.Foundation.Heat.heatConv t (CKN.spatialLaplacian f) x) t
A smooth compact input evolves by the heat equation under Gaussian convolution.
theorem
ESS.heatConv_spatialLaplacian_input
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hfc : HasCompactSupport f)
{t : ℝ}
(ht : 0 < t)
(x : CKN.Foundation.Parabolic.Vec3)
:
Spatial differentiation of a smooth Gaussian heat orbit commutes with the Laplacian on its compactly supported input.
theorem
ESS.heatConvVec3_component_hasDerivAt_laplacianInput
{b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i)
(hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i)
{t : ℝ}
(ht : 0 < t)
(x : CKN.Foundation.Parabolic.Vec3)
(i : Fin 3)
:
HasDerivAt (fun (s : ℝ) => heatConvVec3 s b x i)
(CKN.Foundation.Heat.heatConv t (CKN.spatialLaplacian fun (y : CKN.Foundation.Parabolic.Vec3) => b y i) x) t
Each component of a smooth compact vector heat orbit satisfies the heat equation.
theorem
ESS.heatConvVec3_component_spatialLaplacian_input
{b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i)
(hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i)
{t : ℝ}
(ht : 0 < t)
(x : CKN.Foundation.Parabolic.Vec3)
(i : Fin 3)
:
CKN.spatialLaplacian (fun (z : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b z i) x = CKN.Foundation.Heat.heatConv t (CKN.spatialLaplacian fun (y : CKN.Foundation.Parabolic.Vec3) => b y i) x
The spatial Laplacian of each component of a smooth compact vector heat orbit is convolution with the input Laplacian.