Weak formulation of the smooth forced heat response

For a smooth compactly supported tensor supported in positive times, the forced heat response satisfies, against every smooth compactly supported test function, the weak gradient identity and the weak form of the heat equation ∫∫ -Z_i ∂_t φ + ∑_j ∂_j Z_i ∂_j φ + ∑_j G_ij ∂_j φ = 0 used in lem:pv-stokes.

theorem ESS.instIsAddHaarMeasureProdVec3RealVolume_2 : MeasureTheory.volume.IsAddHaarMeasure

theorem ESS.integral_mul_fderiv_test {f ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ 1 f) (hψ : ContDiff ℝ 1 ψ) (hψc : HasCompactSupport ψ) (v : CKN.Foundation.Parabolic.Vec3 × ℝ) : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), f p * (fderiv ℝ ψ p) v = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), (fderiv ℝ f p) v * ψ p

Integration by parts on Vec3 × ℝ against a smooth compactly supported test function.

theorem ESS.response_weak_equation {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ∀ (i j : Fin 3), ContDiff ℝ (↑⊤) (g i j)) (hgc : ∀ (i j : Fin 3), HasCompactSupport (g i j)) {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (i : Fin 3) : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), -(causalHeatConv (vecTimeDiv g i) p * (fderiv ℝ ψ p) (0, 1)) + ∑ j : Fin 3, (fderiv ℝ (causalHeatConv (vecTimeDiv g i)) p) (CKN.basisVec j, 0) * (fderiv ℝ ψ p) (CKN.basisVec j, 0) + ∑ j : Fin 3, g i j p * (fderiv ℝ ψ p) (CKN.basisVec j, 0) = 0

The weak form of the forced heat equation for smooth compactly supported tensors, on Vec3 × ℝ: for every smooth compactly supported test function, ∫∫ -Z_i ∂_t ψ + ∑_j ∂_j Z_i ∂_j ψ + ∑_j g_ij ∂_j ψ = 0.