Weak time derivatives from pointwise time derivatives

A function on a slab which is differentiable in time at every point of space, whose time derivative is square integrable on every slab strictly inside, has that time derivative as its weak time derivative against smooth compactly supported tests on the slab (prop:lps-local-strong).

theorem ESS.LPS.lps_test_time_margin {a T : ℝ} (hab : a < T) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a T)) : ∃ (a' : ℝ) (b' : ℝ), a < a' ∧ a' < b' ∧ b' < T ∧ ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), z.2 ∉ Set.Ioo a' b' → z ∉ tsupport φ

The time projection of the support of a space-time test function lies in a closed interval strictly inside the time interval.

theorem ESS.LPS.lps_slab_time_weak_of_pointwise {a T : ℝ} (hab : a < T) {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hd : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∀ t ∈ Set.Ioo a T, HasDerivAt (fun (s : ℝ) => f (x, s)) (g (x, t)) t) (hgc : ∀ (x : CKN.Foundation.Parabolic.Vec3), ContinuousOn (fun (s : ℝ) => g (x, s)) (Set.Ioo a T)) (hf : ∀ (a' b' : ℝ), a < a' → a' < b' → b' < T → MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (CKN.vlSlab a' b'))) (hg : ∀ (a' b' : ℝ), a < a' → a' < b' → b' < T → MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (CKN.vlSlab a' b'))) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a T)) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a T, f z * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a T, g z * φ z

A function differentiable in time at every point of space, with time derivative square integrable on every slab strictly inside, has that derivative as weak time derivative on the slab (prop:lps-local-strong).

theorem ESS.LPS.lps_regR12_velocity_memLp_slab (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {δ T : ℝ} (hδ : 0 < δ) (hδT : δ < T) (i : Fin 3) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => lpsRegU ρ ε hε b hb z i) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo δ T)))

The regularized velocity is square integrable on every positive-time slab (thm:regularised of the CKN manuscript, (R3)).

theorem ESS.LPS.lps_regR12_weak_time (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {T : ℝ} (hT : 0 < T) (i : Fin 3) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab 0 T, lpsRegU ρ ε hε b hb (z.1, z.2) i * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab 0 T, lpsRegQ ρ ε hε b hb (z.1, z.2) i * φ z

The regularized velocity has its momentum right-hand side as weak time derivative on every slab ℝ³ × (0, T) (thm:regularised of the CKN manuscript, (R2)).