Tensor energy estimates on spatial slices #
The mean oscillation estimate behind eq:Chat controls the tensor energy
in eq:pressure-gradient-morrey by the velocity cube. The mean oscillation
argument follows the local estimate in CKN.Pressure.Lin34SliceMeanFree.
theorem
CKN.Core.Step4.origin_slice_mean_free_cube_bound
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x : Foundation.Parabolic.Vec3}
{r s : ℝ}
(hr : 0 < r)
(hu :
MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (Foundation.Parabolic.vec3Ball x r)
MeasureTheory.volume)
(hu3 :
MeasureTheory.IntegrableOn
(fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 3)
(Foundation.Parabolic.vec3Ball x r) MeasureTheory.volume)
:
∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x r, ENNReal.ofReal
(Foundation.Parabolic.vec3EuclideanNorm
(u (y, s) - ⨍ (z : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x r, u (z, s))) ^ 3 ≤ 8 * ∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (y, s))) ^ 3
The spatial mean-free velocity cube is at most eight times the raw cube.
theorem
CKN.Core.Step4.origin_slice_tensor_energy_bound
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x : Foundation.Parabolic.Vec3}
{r s : ℝ}
(hr : 0 < r)
(hu :
MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (Foundation.Parabolic.vec3Ball x r)
MeasureTheory.volume)
(hu3 :
MeasureTheory.IntegrableOn
(fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 3)
(Foundation.Parabolic.vec3Ball x r) MeasureTheory.volume)
:
∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x r, ENNReal.ofReal (utensorNorm u x r s y) ^ (3 / 2) ≤ 8 ^ (1 / 2) * ∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (y, s))) ^ 3
The tensor's three-halves energy is bounded by the velocity cube, with the square root of eight from subtraction of the spatial average.
theorem
CKN.Core.Step4.origin_tensor_energy_time_bound
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x : Foundation.Parabolic.Vec3}
{r : ℝ}
{J : Set ℝ}
(hr : 0 < r)
(hu :
MeasureTheory.Integrable u
((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)).prod (MeasureTheory.volume.restrict J)))
(hu3 :
MeasureTheory.Integrable (fun (w : Foundation.Parabolic.Vec3 × ℝ) => Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 3)
((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)).prod (MeasureTheory.volume.restrict J)))
:
∫⁻ (s : ℝ) in J, (∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x r, ENNReal.ofReal (utensorNorm u x r s y) ^ (3 / 2)) ^ (4 / 5) ≤ 8 ^ (2 / 5) * (∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in Foundation.Parabolic.vec3Ball x r ×ˢ J, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3) ^ (4 / 5) * MeasureTheory.volume J ^ (1 / 5)
The tensor-energy contribution has the temporal four-fifths estimate on any time window, with the velocity cube integrated on the same box.
theorem
CKN.Core.Step4.origin_real_tensor_energy_time_bound
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x : Foundation.Parabolic.Vec3}
{r : ℝ}
{J : Set ℝ}
(hr : 0 < r)
(hu :
MeasureTheory.Integrable u
((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)).prod (MeasureTheory.volume.restrict J)))
(hu3 :
MeasureTheory.Integrable (fun (w : Foundation.Parabolic.Vec3 × ℝ) => Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 3)
((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)).prod (MeasureTheory.volume.restrict J)))
:
∫⁻ (s : ℝ) in J, ENNReal.ofReal
((∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x r, utensorNorm u x r s y ^ (3 / 2)) ^ (2 / 3)) ^ (6 / 5) ≤ 8 ^ (2 / 5) * (∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in Foundation.Parabolic.vec3Ball x r ×ˢ J, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3) ^ (4 / 5) * MeasureTheory.volume J ^ (1 / 5)
The real tensor energy used in the harmonic slice bound satisfies the
same time estimate after taking its two-thirds power and then 6/5.