The heat equation with source for a strong solution

prop:lps-smoothing: with G = ∂ₜu - Δu (in L²), each velocity component of a strong solution is a distributional solution of ∂ₜ uᵢ - Δ uᵢ = Gᵢ on the slab.

theorem ESS.lps_strong_isHeatSolution {t₀ T : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hderiv : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hDtu : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (i : Fin 3) : CKN.IsHeatSolutionOn Set.univ (Set.Ioo t₀ T) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i) fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Dtu z i - ∑ j : Fin 3, D2u z i j j

Each velocity component of a strong solution solves the heat equation with source Dtu - Δu in distributions on the slab (prop:lps-smoothing).