The H² energy of the slices of a strong solution

prop:lps-smoothing: the sum of the squared H² norms of the velocity slices is integrable in time, and bounds the pointwise square of each velocity component almost everywhere.

noncomputable def ESS.lpsSliceH2 (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) (t : ℝ) : ℝ

The squared H² norm of the velocity slice at time t.

Equations

• ESS.lpsSliceH2 u Du D2u t = ∑ i : Fin 3, ∑ α ∈ CKN.sobolevWords 2, ∫ (y : CKN.Foundation.Parabolic.Vec3), ESS.lpsStrongFamily u Du D2u i α (y, t) ^ 2

theorem ESS.lpsSliceH2_nonneg (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) (t : ℝ) : 0 ≤ lpsSliceH2 u Du D2u t

theorem ESS.lps_sliceH2_integrable {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)))) (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)))) : MeasureTheory.Integrable (fun (t : ℝ) => lpsSliceH2 u Du D2u t) (MeasureTheory.volume.restrict (Set.Ioo t₀ T))

The slice H² energy is integrable on the time interval (prop:lps-smoothing).

theorem ESS.lps_ae_slice_sup_bound_strong : ∃ (K : ℝ), 0 ≤ K ∧ ∀ {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}, CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu → MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))) → MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))) → MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))) → ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ T), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∀ (i : Fin 3), u (x, t) i ^ 2 ≤ K * lpsSliceH2 u Du D2u t

Almost every slice of the velocity is bounded pointwise by a universal multiple of its H² energy (prop:lps-smoothing).