Velocity slices for the fixed pressure split #
The assumed essential supremum of the local cubic velocity mass controls the
whole-space L³ norms of its zero-extended spatial slices.
noncomputable def
ESS.pressureSplitVelocityLpBound
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
:
The L³ slice bound associated with the local cubic velocity mass in
lem:pressure-split.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
ESS.pressureSplitVelocityExtension
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
:
The velocity on each time slice, extended by zero outside the source ball.
Equations
- ESS.pressureSplitVelocityExtension u z = ESS.pressureSplitBall.indicator (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, z.2)) z.1
Instances For
theorem
ESS.pressureSplitVelocityExtension_slice_memLp_bound
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict pressureSplitDomain))
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in pressureSplitBall, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict pressureSplitTime) < ⊤)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict pressureSplitTime, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => pressureSplitVelocityExtension u (x, t)) 3
MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => pressureSplitVelocityExtension u (x, t)) 3
MeasureTheory.volume ≤ ENNReal.ofReal (pressureSplitVelocityLpBound u)
Almost every zero-extended velocity slice belongs to L³ and has norm
bounded by pressureSplitVelocityLpBound.