Multi-index derivatives on time slices of Ω × I

Slice-level calculus for multiPartial used in the proof of thm:analytic:interior: joint smoothness gives smoothness of time slices, spatial partials commute, ∂^α (∂_j g) = ∂^{α+e_j} g, and the Laplacian commutes with ∂^α.

theorem CIV.contDiffOn_slice_of_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) {t : ℝ} (ht : t ∈ I) : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)) Ω

A jointly smooth field on Ω × I has smooth time slices.

theorem CIV.contDiffOn_slice_spatialPartial {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} (hΩ : IsOpen Ω) (t : ℝ) (hG : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)) Ω) (j : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.spatialPartial g j (x, t)) Ω

The time slice of a spatial partial derivative is smooth.

theorem CIV.spatialPartial_comm_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} (hΩ : IsOpen Ω) (t : ℝ) (hG : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)) Ω) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ Ω) (i j : Fin 3) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial g i w) j (x, t) = CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial g j w) i (x, t)

Spatial partial derivatives commute on a time slice.

theorem CIV.multiPartial_spatialPartial_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} (hΩ : IsOpen Ω) (t : ℝ) (hG : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)) Ω) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ Ω) (α : Fin 3 → ℕ) (j : Fin 3) : multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial g j w) α (x, t) = multiPartial g (α + Pi.single j 1) (x, t)

∂^α (∂_j g) = ∂^{α + e_j} g on a time slice.

theorem CIV.sum_spatialSecondPartial_multiPartial_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} (hΩ : IsOpen Ω) (t : ℝ) (hG : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)) Ω) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ Ω) (α : Fin 3 → ℕ) : ∑ j : Fin 3, CKN.spatialSecondPartial (multiPartial g α) j j (x, t) = multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, CKN.spatialSecondPartial g j j w) α (x, t)

The Laplacian commutes with ∂^α on a time slice.