The causal space-time heat potential

For a smooth compactly supported space-time source h, the convolution of the causal heat kernel heatKernelPlus with h is smooth, commutes with derivatives, and solves the forward heat equation with source h. These are the smooth-data facts behind the zero-data response of lem:pv-stokes.

theorem ESS.instIsAddHaarMeasureProdVec3RealVolume : MeasureTheory.volume.IsAddHaarMeasure

noncomputable def ESS.causalHeatConv (h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (v : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The causal heat potential W₊ ⋆ h of a space-time source h, the Duhamel solution with zero data used in lem:pv-stokes.

Equations

• ESS.causalHeatConv h v = MeasureTheory.convolution (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Heat.heatKernelPlus p) h (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume v

theorem ESS.causalHeatConv_eq_integral (h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (v : CKN.Foundation.Parabolic.Vec3 × ℝ) : causalHeatConv h v = ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Heat.heatKernelPlus p * h (v - p)

The causal heat potential as an explicit space-time integral.

theorem ESS.causalHeatConv_contDiff {h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : ContDiff ℝ (↑⊤) h) (hc : HasCompactSupport h) : ContDiff ℝ (↑⊤) (causalHeatConv h)

The causal heat potential of a smooth compactly supported source is smooth.

theorem ESS.causalHeatConv_fderiv_apply {h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : ContDiff ℝ (↑⊤) h) (hc : HasCompactSupport h) (v w : CKN.Foundation.Parabolic.Vec3 × ℝ) : (fderiv ℝ (causalHeatConv h) v) w = causalHeatConv (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ h q) w) v

Derivatives of the causal heat potential fall on the source.

theorem ESS.contDiff_fderiv_apply_const {h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : ContDiff ℝ (↑⊤) h) (w : CKN.Foundation.Parabolic.Vec3 × ℝ) : ContDiff ℝ ↑⊤ fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ h q) w

A directional derivative of a smooth compactly supported function is again smooth and compactly supported.

theorem ESS.fderiv_comp_sub_left_apply {F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Differentiable ℝ F) (v p w : CKN.Foundation.Parabolic.Vec3 × ℝ) : (fderiv ℝ (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => F (v - q)) p) w = -(fderiv ℝ F (v - p)) w

Differentiating q ↦ F (v - q) reverses the direction.

theorem ESS.heatKernelPlus_backward_heat_pairing {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : (-∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Heat.heatKernelPlus z * (fderiv ℝ ψ z) (0, 1)) - ∑ i : Fin 3, ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Heat.heatKernelPlus z * (fderiv ℝ (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ ψ q) (CKN.basisVec i, 0)) z) (CKN.basisVec i, 0) = ψ (0, 0)

The causal heat kernel is a fundamental solution of the heat operator: pairing it with the backward heat operator applied to a smooth compactly supported function returns the value at the origin.

theorem ESS.causalHeatConv_heat_equation {h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : ContDiff ℝ (↑⊤) h) (hc : HasCompactSupport h) (v : CKN.Foundation.Parabolic.Vec3 × ℝ) : (fderiv ℝ (causalHeatConv h) v) (0, 1) - ∑ i : Fin 3, (fderiv ℝ (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ (causalHeatConv h) q) (CKN.basisVec i, 0)) v) (CKN.basisVec i, 0) = h v

The causal heat potential solves the forward heat equation with source h, written with directional derivatives on Vec3 × ℝ.

theorem ESS.causalHeatConv_eq_zero_of_nonpos {h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hpos : ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), h p ≠ 0 → 0 < p.2) {v : CKN.Foundation.Parabolic.Vec3 × ℝ} (hv : v.2 ≤ 0) : causalHeatConv h v = 0

A source supported in positive times has a causal heat potential that vanishes at nonpositive times.