The zero-data forced heat response in kernel form

For a tensor source G, the response Z_i = ∑_j ∂_j W₊ ⋆ G_ij solves the componentwise heat equation ∂_t Z_i - Δ Z_i = ∑_j ∂_j G_ij with zero data; this is the scalar reformulation of lem:pv-stokes once the pressure is folded into the source. For smooth compactly supported sources an integration by parts in space moves the derivative onto the source, which identifies the response with the causal heat potential of the divergence.

theorem ESS.instIsAddHaarMeasureProdVec3RealVolume_1 : MeasureTheory.volume.IsAddHaarMeasure

noncomputable def ESS.forcedHeat (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.Vec3

The zero-data forced heat response of a space-time tensor G: Z_i(z) = ∫ ∑_j ∂_j W₊(p) G_ij(z - p) dp, the kernel form of the Duhamel formula used in lem:pv-stokes.

Equations

• ESS.forcedHeat G z i = ∫ (p : CKN.Foundation.Parabolic.ParabolicPoint), ∑ j : Fin 3, CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j * G i j (z.1 - p.1, z.2 - p.2)

theorem ESS.heatKernelSpaceDerivative_vecTime_measurable (j : Fin 3) : Measurable fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j

Each spatial derivative of the causal heat kernel is measurable on Vec3 × ℝ.

theorem ESS.heatKernelSpaceDerivative_locallyIntegrable (j : Fin 3) : MeasureTheory.LocallyIntegrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j) MeasureTheory.volume

Each spatial derivative of the causal heat kernel is locally integrable on Vec3 × ℝ.

theorem ESS.heatKernelSpaceDerivative_convolution_eq {g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (v : CKN.Foundation.Parabolic.Vec3 × ℝ) (j : Fin 3) : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j * g (v - p) = ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Heat.heatKernelPlus p * (fderiv ℝ g (v - p)) (CKN.basisVec j, 0)

Integration by parts in space: the spatial-derivative kernel against a smooth compactly supported source equals the causal heat kernel against the spatial derivative of the source.

theorem ESS.forcedHeat_eq_causalHeatConv {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG : ∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (hGc : ∀ (i j : Fin 3), HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (i : Fin 3) : (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => forcedHeat G z i) = causalHeatConv fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ j : Fin 3, CKN.spatialPartial (G i j) j q

For a smooth compactly supported tensor, the forced heat response is the causal heat potential of the tensor divergence ∑_j ∂_j G_ij.

theorem ESS.tensorDivergence_contDiff {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG : ∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ j : Fin 3, CKN.spatialPartial (G i j) j q

The tensor divergence of a smooth compactly supported tensor is smooth.

theorem ESS.tensorDivergence_hasCompactSupport {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG : ∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (hGc : ∀ (i j : Fin 3), HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (i : Fin 3) : HasCompactSupport fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ j : Fin 3, CKN.spatialPartial (G i j) j q

The tensor divergence of a compactly supported smooth tensor has compact support.

theorem ESS.forcedHeat_contDiff {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG : ∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (hGc : ∀ (i j : Fin 3), HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => forcedHeat G z i

The forced heat response of a smooth compactly supported tensor is smooth on Vec3 × ℝ.

theorem ESS.forcedHeat_eq_zero_of_nonpos {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hGpos : ∀ (i j : Fin 3) (p : CKN.Foundation.Parabolic.ParabolicPoint), G i j p ≠ 0 → 0 < p.2) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z.2 ≤ 0) : forcedHeat G z = 0

The forced heat response of a tensor vanishing at nonpositive times is zero at nonpositive times: the response has zero initial data.