Heat equations for spatial derivatives

If ∂ₜ u - Δ u = g in distributions on ℝ³ × I and U_k is the distributional derivative ∂_k u, then ∂ₜ U_k - Δ U_k = ∂_k g in divergence form, and in source form when ∂_k g is a function. Iterating along the words of a space-time derivative family gives the equations for all spatial derivatives of a solution up to the order of its source.

theorem ESS.spatialPartial_neg_of_contDiff {A : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => -A q) j p = -CKN.spatialPartial A j p

theorem ESS.spatialPartial_backwardHeat {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (k : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => -CKN.timePartial φ q - ∑ j : Fin 3, CKN.spatialSecondPartial φ j j q) k p = -CKN.timePartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial φ k q) p - ∑ j : Fin 3, CKN.spatialSecondPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial φ k q) j j p

The spatial derivative of the backward heat operator applied to a test function is the backward heat operator applied to its spatial derivative.

theorem ESS.heatSolution_deriv_flux {I : Set ℝ} {u g Uk : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {k : Fin 3} (hheat : CKN.IsHeatSolutionOn Set.univ I u g) (hk : IsSpaceTimeWeakPartial (Set.univ ×ˢ I) k u Uk) (φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ Set.univ ×ˢ I → ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ I, Uk p * (-CKN.timePartial φ p - ∑ j : Fin 3, CKN.spatialSecondPartial φ j j p) = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ I, g p * CKN.spatialPartial φ k p

A spatial derivative of a solution with source g solves the heat equation with the divergence-form source ∂_k g.

theorem ESS.heatSolution_deriv_source {I : Set ℝ} {u g Uk gk : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {k : Fin 3} (hheat : CKN.IsHeatSolutionOn Set.univ I u g) (hk : IsSpaceTimeWeakPartial (Set.univ ×ˢ I) k u Uk) (hgk : IsSpaceTimeWeakPartial (Set.univ ×ˢ I) k g gk) : CKN.IsHeatSolutionOn Set.univ I Uk gk

If moreover ∂_k g is a function, the derivative solves the heat equation with source ∂_k g.

theorem ESS.heatSolution_family_source {I : Set ℝ} {m : ℕ} {Dw DH : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hw : IsSpaceTimeFamily m (Set.univ ×ˢ I) Dw) (hH : IsSpaceTimeFamily (m - 1) (Set.univ ×ˢ I) DH) (hheat : CKN.IsHeatSolutionOn Set.univ I (Dw []) (DH [])) (β : List (Fin 3)) : β.length ≤ m - 1 → CKN.IsHeatSolutionOn Set.univ I (Dw β) (DH β)

The heat equations along a derivative family, through the order of the source.

theorem ESS.heatSolution_family_flux {I : Set ℝ} {m : ℕ} {Dw DH : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hw : IsSpaceTimeFamily m (Set.univ ×ˢ I) Dw) (hH : IsSpaceTimeFamily (m - 1) (Set.univ ×ˢ I) DH) (hheat : CKN.IsHeatSolutionOn Set.univ I (Dw []) (DH [])) (hm : 1 ≤ m) (β : List (Fin 3)) (hβ : β.length ≤ m - 1) (k : Fin 3) (φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ Set.univ ×ˢ I → ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ I, Dw (β ++ [k]) p * (-CKN.timePartial φ p - ∑ j : Fin 3, CKN.spatialSecondPartial φ j j p) = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ I, DH β p * CKN.spatialPartial φ k p

The top-order heat equations in divergence form.