Space-time Sobolev families of the Leray projection

prop:lps-smoothing: if a vector field B lies in L²(I; H^M(ℝ³)), with space-time derivative families DB, then the time slices of the Leray projection -P B(t) form a field in L²(I; H^M(ℝ³)): for each word α the curve t ↦ -P(DB α)(t) of L² classes is measurable, and a jointly measurable representative gives the derivative family. The projection commutes with weak derivatives and does not increase L² norms, so the new family satisfies the weak derivative relations and has norm at most that of DB.

theorem ESS.lps_exists_slice_curve {a b : ℝ} (F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ∃ (γ : ℝ → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)), MeasureTheory.StronglyMeasurable γ ∧ (MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo a b)) → ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ↑↑(γ t) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t))

A square-integrable function on a slab has a strongly measurable curve of L²(ℝ³) classes agreeing with almost every time slice (prop:lps-smoothing).

theorem ESS.lps_stronglyMeasurable_field_curve {γ : Fin 3 → ℝ → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)} (hγ : ∀ (k : Fin 3), MeasureTheory.StronglyMeasurable (γ k)) : MeasureTheory.StronglyMeasurable fun (t : ℝ) => WithLp.toLp 2 fun (k : Fin 3) => γ k t

A curve of fields in L²(ℝ³; ℝ³) whose three components are strongly measurable curves is strongly measurable (prop:lps-smoothing).

theorem ESS.lps_leray_l2SobolevFamily {a b : ℝ} {M : ℕ} {f g : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {DB : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hB : ∀ (k : Fin 3), CKN.IsL2SobolevFamilyOn M Set.univ (Set.Ioo a b) (f k) (DB k)) (hgm : ∀ (i : Fin 3), MeasureTheory.AEStronglyMeasurable (g i) (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo a b))) (hg : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (i : Fin 3) (hf : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => f k (y, t)) 2 MeasureTheory.volume), (fun (x : CKN.Foundation.Parabolic.Vec3) => g i (x, t)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => -lpsLerayApply (fun (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) => f k (y, t)) hf i x) : ∃ (DG : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (i : Fin 3), CKN.IsL2SobolevFamilyOn M Set.univ (Set.Ioo a b) (g i) (DG i)) ∧ ∑ i : Fin 3, CKN.l2SobolevNormSqOn M Set.univ (Set.Ioo a b) (DG i) ≤ ∑ i : Fin 3, CKN.l2SobolevNormSqOn M Set.univ (Set.Ioo a b) (DB i)

prop:lps-smoothing: the Leray projection of a field in L²(I; H^M(ℝ³)). If the three components f k have space-time derivative families DB k through order M on ℝ³ × (a, b), and almost every time slice of g is the negative Leray projection of the slice of f, then g has space-time derivative families through order M whose total squared norm is at most that of DB.

theorem ESS.lps_source_family {t₀ T : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsLpsStrongSolution t₀ T u Du p) (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)))) (hDu : MeasureTheory.MemLp Du 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)))) {a b : ℝ} (ha : t₀ ≤ a) (hb : b ≤ T) {M : ℕ} (DB : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hB : ∀ (i : Fin 3), CKN.IsL2SobolevFamilyOn M Set.univ (Set.Ioo a b) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ j : Fin 3, u z j * Du z i j) (DB i)) : ∃ (DG : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (i : Fin 3), CKN.IsL2SobolevFamilyOn M Set.univ (Set.Ioo a b) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Dtu z i - ∑ j : Fin 3, D2u z i j j) (DG i)) ∧ ∑ i : Fin 3, CKN.l2SobolevNormSqOn M Set.univ (Set.Ioo a b) (DG i) ≤ ∑ i : Fin 3, CKN.l2SobolevNormSqOn M Set.univ (Set.Ioo a b) (DB i)

prop:lps-smoothing: the source of a strong solution in L²(I; H^M). On a time interval (a, b) ⊆ (t₀, T), if the convection field (u·∇)u, with components Σⱼ uⱼ ∂ⱼuᵢ, has space-time derivative families DB through order M, then so does the source ∂ₜu - Δu = -P((u·∇)u), with total squared L²(I; H^M) norm at most that of DB.