Mixed partial derivatives on an open product Ω × I

The smoothness of classical partial derivatives and the symmetry of mixed space and time partial derivatives for a jointly smooth scalar field on an open space-time product. These are the forms used on the cylinder B(R) × (t₁, t₂) of thm:analytic:interior.

theorem CIV.contDiffOn_spatialPartial_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial g i z) (CKN.spaceTimeSet Ω I)

If a scalar field is jointly smooth on the open set Ω × I, so is each of its classical spatial partial derivatives.

theorem CIV.contDiffOn_timePartial_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.timePartial g z) (CKN.spaceTimeSet Ω I)

If a scalar field is jointly smooth on the open set Ω × I, so is its classical time partial derivative.

theorem CIV.spatialSecondPartial_eq_jointFDeriv2_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ CKN.spaceTimeSet Ω I) (i j : Fin 3) : CKN.spatialSecondPartial g i j z = ((fderiv ℝ (fderiv ℝ fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => g w) z) (CKN.basisVec j, 0)) (CKN.basisVec i, 0)

theorem CIV.spatialSecondPartial_comm_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ CKN.spaceTimeSet Ω I) (i j : Fin 3) : CKN.spatialSecondPartial g i j z = CKN.spatialSecondPartial g j i z

Cartesian mixed spatial partials of a jointly smooth scalar field commute.

theorem CIV.spatialPartial_timePartial_eq_jointFDeriv2_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ CKN.spaceTimeSet Ω I) (i : Fin 3) : CKN.spatialPartial (CKN.timePartial g) i z = ((fderiv ℝ (fderiv ℝ fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => g w) z) (CKN.basisVec i, 0)) (0, 1)

theorem CIV.timePartial_spatialPartial_eq_jointFDeriv2_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ CKN.spaceTimeSet Ω I) (i : Fin 3) : CKN.timePartial (CKN.spatialPartial g i) z = ((fderiv ℝ (fderiv ℝ fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => g w) z) (0, 1)) (CKN.basisVec i, 0)

theorem CIV.spatialPartial_timePartial_comm_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ CKN.spaceTimeSet Ω I) (i : Fin 3) : CKN.spatialPartial (CKN.timePartial g) i z = CKN.timePartial (CKN.spatialPartial g i) z

The classical spatial and time partial derivatives of a jointly smooth scalar field commute.