The projected equation on almost every time slice #
prop:lps-smoothing: for a strong solution, at almost every time t the field
G(t) = (∂ₜu - Δu)(t) is weakly divergence free, and G(t) + ((u·∇)u)(t) is the gradient
of the pressure slice up to sign. Applying the Leray projection P gives
G(t) = -P((u·∇)u)(t).
theorem
ESS.lpsLerayApply_add
{g h : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ}
(hg : ∀ (j : Fin 3), MeasureTheory.MemLp (g j) 2 MeasureTheory.volume)
(hh : ∀ (j : Fin 3), MeasureTheory.MemLp (h j) 2 MeasureTheory.volume)
(i : Fin 3)
:
lpsLerayApply (fun (j : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) => g j x + h j x) ⋯ i =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => lpsLerayApply g hg i x + lpsLerayApply h hh i x
The Leray projection of a sum of fields is the sum of the projections
(prop:lps-smoothing).
theorem
ESS.lps_strong_slice_projected_equation
{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))))
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ T), ∀ (i : Fin 3)
(hconv :
∀ (i' : Fin 3),
MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, u (y, t) j * Du (y, t) i' j) 2
MeasureTheory.volume),
(fun (x : CKN.Foundation.Parabolic.Vec3) => Dtu (x, t) i - ∑ j : Fin 3, D2u (x, t) i j j) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) =>
-lpsLerayApply (fun (i' : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, u (y, t) j * Du (y, t) i' j)
hconv i x
prop:lps-smoothing: the projected equation on almost every time slice. For almost every
time t, (∂ₜu - Δu)(t) = -P((u·∇)u)(t) almost everywhere on ℝ³, where Δu = Σⱼ ∂ⱼ∂ⱼu,
((u·∇)u)ᵢ = Σⱼ uⱼ ∂ⱼuᵢ and P is the Leray projection lpsLerayP acting through
lpsLerayApply.