Trace Initial L3 #
The strong initial trace inherits an almost-every-time critical L³ bound
(paper label lem:pv-initial-l3).
theorem
ESS.lerayHopf_initialTrace_memLp_three
{T : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hLH : CKN.IsLerayHopfSolution T a u Du)
(M : ENNReal)
(hM : M < ⊤)
(hL3 :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)))
(ENNReal.ofReal 3) MeasureTheory.volume ≤ M)
:
The strong initial trace inherits an almost-every-time critical L³ bound
(paper label lem:pv-initial-l3).