Weak identities of smooth forced heat responses on the slab

For a smooth compactly supported tensor supported in positive times and a smooth test function compactly supported in the slab Q_τ, the forced heat response satisfies on Q_τ, in the CKN derivative conventions, the weak gradient identity ∫ Z_i ∂_j φ = -∫ ∂_j Z_i φ and the weak heat equation ∫ -Z_i ∂_t φ + ∑_j ∂_j Z_i ∂_j φ + ∑_j G_ij ∂_j φ = 0 of lem:pv-stokes.

theorem ESS.spatialPartial_forcedHeat_sub {G 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) (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 j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => forcedHeat (G - G') w i) j z = CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => forcedHeat G w i) j z - CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => forcedHeat G' w i) j z

The spatial derivatives of a smooth forced heat response are differences of those of its tensors: ∂_j (Z(G) - Z(G'))_i = ∂_j Z(G)_i - ∂_j Z(G')_i.

theorem ESS.forcedHeat_smooth_weak_slab {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) {τ : ℝ} {φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) (hφc : HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) (hφQ : (tsupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) ⊆ Set.univ ×ˢ Set.Ioo 0 τ) (i : Fin 3) : (∀ (j : Fin 3), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), forcedHeat G z i * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => forcedHeat G w i) j z * φ z) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), -(forcedHeat G z i * CKN.timePartial φ z) + ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => forcedHeat G w i) j z * CKN.spatialPartial φ j z + ∑ j : Fin 3, G i j z * CKN.spatialPartial φ j z = 0

The weak gradient identity and the weak heat equation on the slab for the forced heat response of a smooth compactly supported tensor, against smooth tests compactly supported in the slab.