Differentiation formulas for the heat kernel

The coordinate formulas below use the standard coordinate directions of Fin 3 → ℝ. They do not use the function space's ambient norm; all spatial quadratic expressions are finite sums.

noncomputable def CKN.Foundation.Heat.heatKernelTimeDerivative (x : Parabolic.Vec3) (t : ℝ) : ℝ

Time derivative formula for the causal heat kernel.

Equations

• CKN.Foundation.Heat.heatKernelTimeDerivative x t = if 0 < t then CKN.Foundation.Heat.heatKernel x t * ((∑ i : Fin 3, x i ^ 2) / (4 * t ^ 2) - 3 / (2 * t)) else 0

noncomputable def CKN.Foundation.Heat.heatKernelSpaceDerivative (x : Parabolic.Vec3) (t : ℝ) (i : Fin 3) : ℝ

First spatial derivative formula for the causal heat kernel.

Equations

• CKN.Foundation.Heat.heatKernelSpaceDerivative x t i = if 0 < t then -x i / (2 * t) * CKN.Foundation.Heat.heatKernel x t else 0

noncomputable def CKN.Foundation.Heat.heatKernelSpaceSecondDerivative (x : Parabolic.Vec3) (t : ℝ) (i : Fin 3) : ℝ

Pure second spatial derivative formula for the causal heat kernel.

Equations

• CKN.Foundation.Heat.heatKernelSpaceSecondDerivative x t i = if 0 < t then (x i ^ 2 / (4 * t ^ 2) - 1 / (2 * t)) * CKN.Foundation.Heat.heatKernel x t else 0

noncomputable def CKN.Foundation.Heat.heatKernelSpaceMixedSecondDerivative (x : Parabolic.Vec3) (t : ℝ) (i j : Fin 3) : ℝ

Mixed second spatial derivative formula for the causal heat kernel.

Equations

• CKN.Foundation.Heat.heatKernelSpaceMixedSecondDerivative x t i j = if 0 < t then (x i * x j / (4 * t ^ 2) - if i = j then 1 / (2 * t) else 0) * CKN.Foundation.Heat.heatKernel x t else 0

noncomputable def CKN.Foundation.Heat.heatKernelSpaceThirdDerivative (x : Parabolic.Vec3) (t : ℝ) (i j k : Fin 3) : ℝ

Third spatial derivative formula for the causal heat kernel.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Foundation.Heat.heatKernelSpaceFourthDerivative (x : Parabolic.Vec3) (t : ℝ) (i j k l : Fin 3) : ℝ

Fourth spatial derivative formula for the causal heat kernel.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Foundation.Heat.heatKernelLaplacian (x : Parabolic.Vec3) (t : ℝ) : ℝ

Spatial Laplacian of the heat kernel, summed over coordinate directions.

Equations

• CKN.Foundation.Heat.heatKernelLaplacian x t = ∑ i : Fin 3, CKN.Foundation.Heat.heatKernelSpaceSecondDerivative x t i

theorem CKN.Foundation.Heat.heatKernel_contDiffOn_pos : ContDiffOn ℝ ⊤ (fun (p : Parabolic.Vec3 × ℝ) => heatKernel p.1 p.2) (Set.univ ×ˢ Set.Ioi 0)

theorem CKN.Foundation.Heat.heatKernel_time_differentiableAt {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) : DifferentiableAt ℝ (fun (s : ℝ) => heatKernel x s) t

theorem CKN.Foundation.Heat.heatKernel_time_deriv {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) : deriv (fun (s : ℝ) => heatKernel x s) t = heatKernelTimeDerivative x t

theorem CKN.Foundation.Heat.heatKernel_space_deriv {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) (i : Fin 3) : deriv (fun (s : ℝ) => heatKernel (Function.update x i s) t) (x i) = heatKernelSpaceDerivative x t i

theorem CKN.Foundation.Heat.coord_fderiv_eq_deriv_update {f : Parabolic.Vec3 → ℝ} {x : Parabolic.Vec3} (hf : DifferentiableAt ℝ f x) (i : Fin 3) : (fderiv ℝ f x) (basisVec i) = deriv (fun (s : ℝ) => f (Function.update x i s)) (x i)

theorem CKN.Foundation.Heat.heatKernel_fderiv_apply_basisVec {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) (i : Fin 3) : (fderiv ℝ (fun (z : Parabolic.Vec3) => heatKernel z t) x) (basisVec i) = heatKernelSpaceDerivative x t i

theorem CKN.Foundation.Heat.heatKernel_heat_equation {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) : heatKernelTimeDerivative x t = heatKernelLaplacian x t