Smooth approximation of a rough forced heat response

A tensor in L^{5/2} ∩ L² supported in the slab Q_τ is approximated in both norms by smooth compactly supported tensors supported in positive times, whose forced heat responses converge almost everywhere on the slab to the forced heat response of the tensor. This is the approximation step of lem:pv-stokes.

theorem ESS.forcedHeat_rough_approx {τ : ℝ} (hτ : 0 < τ) {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG52 : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (5 / 2)) MeasureTheory.volume) (hG2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 MeasureTheory.volume) (hGsupp : ∀ (i j : Fin 3), ∀ z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), G i j z = 0) : ∃ (Gn : ℕ → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ), (∀ (n : ℕ) (i j : Fin 3), ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => Gn n i j p) ∧ (∀ (n : ℕ) (i j : Fin 3), HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => Gn n i j p) ∧ (∀ (n : ℕ) (i j : Fin 3), (tsupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => Gn n i j p) ⊆ {p : CKN.Foundation.Parabolic.Vec3 × ℝ | 0 < p.2}) ∧ (∀ (i j : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => Gn n i j p - G i j p) (ENNReal.ofReal (5 / 2)) MeasureTheory.volume) Filter.atTop (nhds 0)) ∧ (∀ (i j : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => Gn n i j p - G i j p) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) ∧ ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo 0 τ), Filter.Tendsto (fun (n : ℕ) => forcedHeat (Gn n) z) Filter.atTop (nhds (forcedHeat G z))

Smooth approximation of a rough tensor with almost everywhere convergence of the forced heat responses on the slab.