Velocity slices and compact tensor sources #
The slice Sobolev estimate and the nine-component tensor estimate supply
ext:CZ in the proof of thm:B. These names retain the endgame interface for
the estimates proved in CKN.Pressure.SliceVelocityCube.
theorem
CKN.Core.Endgame.velocity_norm_memLp_three_on_ball_of_slices
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{ρ t : ℝ}
{Ω' : Set Foundation.Parabolic.Vec3}
(hρ : 0 < ρ)
(hball : Foundation.Parabolic.vec3Ball x₀ ρ ⊆ Ω')
(hts : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 (MeasureTheory.volume.restrict Ω'))
(hDu : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Du (x, t)) 2 (MeasureTheory.volume.restrict Ω'))
(hgrad :
∀ (i : Fin 3),
HasWeakGradientOn Ω' (fun (x : Foundation.Parabolic.Vec3) => u (x, t) i) fun (x : Vec 3) => Du (x, t) i)
:
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (x, t)))
(ENNReal.ofReal 3) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))
Spatial Sobolev slices supply the local L³ input of ext:CZ.
theorem
CKN.Core.Endgame.velocity_norm_memLp_three_ae_on_ball_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}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (x, s)))
(ENNReal.ofReal 3) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ))
Almost every velocity slice has the L³ membership used in ext:CZ.
theorem
CKN.Core.Endgame.pressureUTensor_source_data_of_memLp_three
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{c : ℝ → Foundation.Parabolic.Vec3}
{η : Foundation.Parabolic.Vec3 → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ s : ℝ}
:
0 < ρ →
∀ (hηmeas : MeasureTheory.AEStronglyMeasurable η MeasureTheory.volume) (hηc : HasCompactSupport η)
(hηsupport : tsupport η ⊆ Foundation.Parabolic.vec3Ball x₀ ρ)
(hηbound : ∀ (y : Foundation.Parabolic.Vec3), |η y| ≤ 1)
(humeas :
MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hu :
MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (y, s)))
(ENNReal.ofReal 3) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))),
(∀ (i j : Fin 3),
MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => η y * pressureUTensor u c (y, s) i j)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume) ∧ (∀ (i j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => η y * pressureUTensor u c (y, s) i j) ∧ ∑ i : Fin 3,
∑ j : Fin 3,
MeasureTheory.lpNorm (fun (y : Foundation.Parabolic.Vec3) => η y * pressureUTensor u c (y, s) i j)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ (27 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, pressureUTensorNorm u c s y ^ (3 / 2)) ^ (2 / 3)
The compact tensor source of ext:CZ has L³/² components and the
nine-component norm bound expressed as (27 * E)^(2/3).