The mean-free velocity field on the half-gap collar #
On the collar ball the velocity minus its own spatial slice mean obeys the
L⁶ Sobolev–Poincaré display, so its parabolic Morrey seminorm at the
exponent pair (2, 25/8) — the pair the velocity gradient carries — is
controlled by the gradient slice mass and not by the velocity size. The
volume gain on a cell of radius r beats the Morrey normalisation by
r^{1/10}, uniformly over all cells and both large and small radii.
theorem
CKN.Core.Step4.originASlot_meanFree_L6_le_gradient
(x : Foundation.Parabolic.Vec3)
{r : ℝ}
(hr : 0 < r)
(v : H1Function (euclideanBall x r))
:
MeasureTheory.eLpNorm
(fun (y : Vec 3) => v.toFun y - MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall x r)) v.toFun) 6
(MeasureTheory.volume.restrict (euclideanBall x r)) ≤ sobolevPoincareL6Constant * MeasureTheory.eLpNorm v.grad 2 (MeasureTheory.volume.restrict (euclideanBall x r))
The L⁶ mean-free Sobolev–Poincaré display on a ball.
theorem
CKN.Core.Step4.originASlot_meanFree_L6_ae_of_sws
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
(hr : 0 < r)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - r ^ 2) z.2), ∀ (j : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => u (y, s) j - sourceSliceCentredMean z.1 r u s j) 6
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r)) ≤ sobolevPoincareL6Constant * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, s) j) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r))
Suitable solutions supply the L⁶ mean-free estimate on almost every slice.
theorem
CKN.Core.Step4.originASlot_meanFree_clipped_slice_bound
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(k : Fin 3)
(hpoin :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (j : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => u (y, s) j - sourceSliceCentredMean z.1 ρ u s j) 6
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) ≤ sobolevPoincareL6Constant * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, s) j) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)))
(hmeas :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.AEStronglyMeasurable
(fun (y : Foundation.Parabolic.Vec3) => u (y, s) k - sourceSliceCentredMean z.1 ρ u s k)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)))
(x : Foundation.Parabolic.Vec3)
{rr : ℝ}
(hrr : 0 < rr)
:
∀ᵐ (t : ℝ), MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) =>
(Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator
(fun (w : Foundation.Parabolic.ParabolicPoint) => u w k - sourceSliceCentredMean z.1 ρ u w.2 k) (y, t))
2 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x rr)) ≤ ENNReal.ofReal (min rr ρ) * ENNReal.ofReal (Real.pi * 4 / 3) ^ (1 / 3) * (Set.Ioc (z.2 - ρ ^ 2) z.2).indicator
(fun (t : ℝ) =>
sobolevPoincareL6Constant * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, t) k) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)))
t
The slice bound for the mean-free field on an arbitrary spatial ball.
theorem
CKN.Core.Step4.originASlot_min_radius_scale_le_one
{r ρ : ℝ}
(hr : 0 < r)
(hρ : 0 < ρ)
(hρ1 : ρ ≤ 1)
:
A scaling inequality: the Morrey normalisation absorbs the smaller radius.
theorem
CKN.Core.Step4.originASlot_meanFree_morreyNorm_le
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hρ1 : ρ ≤ 1)
(k : Fin 3)
(hpoin :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (j : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => u (y, s) j - sourceSliceCentredMean z.1 ρ u s j) 6
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) ≤ sobolevPoincareL6Constant * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, s) j) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)))
(hmeas :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.AEStronglyMeasurable
(fun (y : Foundation.Parabolic.Vec3) => u (y, s) k - sourceSliceCentredMean z.1 ρ u s k)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)))
(hGm :
AEMeasurable
((Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
u w k - sourceSliceCentredMean z.1 ρ u w.2 k)
MeasureTheory.volume)
:
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
u w k - sourceSliceCentredMean z.1 ρ u w.2 k) ≤ ENNReal.ofReal (Real.pi * 4 / 3) ^ (1 / 3) * (∫⁻ (t : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, (sobolevPoincareL6Constant * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, t) k) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ))) ^ 2) ^ (1 / 2)
The mean-free field has a gradient-shaped Morrey seminorm at the exponent
pair (2, 25/8), uniformly over all cells.
theorem
CKN.Core.Step4.originASlot_gradient_time_mass_eq
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(k : Fin 3)
(hDm :
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => ‖Du w k‖)
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ)))
(hsl :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => Du (y, t) k)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)))
:
∫⁻ (t : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, t) k) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) ^ 2 = Foundation.Parabolic.Morrey.cylinderPowerIntegral 2 (fun (w : Foundation.Parabolic.ParabolicPoint) => ‖Du w k‖) z ρ
The time integral of the squared slice gradient norms is the cylinder mass.