Ingredients for the local solution bundle

Elementary facts used to assemble the finite-energy weak solution of prop:pv-local-solution from its heat part and its forced part: weak gradients add, the time slices of the heat orbit and their gradients are locally integrable, and the derivatives of a space-time test function are square integrable on the slab.

theorem ESS.hasWeakGradientOn_univ_add {u v : CKN.Foundation.Parabolic.Vec3 → ℝ} {Du Dv : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.LocallyIntegrable u MeasureTheory.volume) (hv : MeasureTheory.LocallyIntegrable v MeasureTheory.volume) (hDu : ∀ (j : Fin 3), MeasureTheory.LocallyIntegrable (fun (x : CKN.Foundation.Parabolic.Vec3) => Du x j) MeasureTheory.volume) (hDv : ∀ (j : Fin 3), MeasureTheory.LocallyIntegrable (fun (x : CKN.Foundation.Parabolic.Vec3) => Dv x j) MeasureTheory.volume) (h1 : CKN.HasWeakGradientOn Set.univ u Du) (h2 : CKN.HasWeakGradientOn Set.univ v Dv) : CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => u x + v x) fun (x : CKN.Vec 3) => Du x + Dv x

Weak gradients on ℝ³ of locally integrable functions add.

theorem ESS.heatOrbit_slice_continuous {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) {s : ℝ} (hs : 0 < s) (i : Fin 3) : Continuous fun (x : CKN.Foundation.Parabolic.Vec3) => heatOrbit a (x, s) i

At a positive time each component of the heat orbit of a square integrable datum is continuous in space.

theorem ESS.heatOrbit_slice_grad_locallyIntegrable {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) {s : ℝ} (hs : 0 < s) (i j : Fin 3) : MeasureTheory.LocallyIntegrable (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatOrbit a (y, s) i) j x) MeasureTheory.volume

At a positive time the spatial derivatives of the heat orbit of a square integrable datum are bounded and measurable, hence locally integrable.

theorem ESS.spaceTimeTest_derivs_memLp_two {φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) (hφc : HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) (σ : ℝ) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.timePartial φ z) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) ∧ ∀ (j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial φ j z) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))

The derivatives of a scalar space-time test function are square integrable on the slab.

theorem ESS.heatOrbit_memLp_two_slab {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : CKN.IsInJ a) {σ : ℝ} (hσ : 0 < σ) : MeasureTheory.MemLp (heatOrbit a) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) ∧ MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatOrbit a (y, z.2) i) j z.1) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))

The heat orbit of a datum in J and its spatial gradient are square integrable on the slab.