Cubic integrability of velocity slices #
The local weak-gradient data of a suitable weak solution give spatial L^6
regularity on almost every ball slice, hence L^3 integrability. The cut-off
velocity tensor then supplies compactly supported L^{3/2} sources for the
unconditional Calderón--Zygmund estimate. The nine-entry source bound retains
its dimension factor by packaging it into the source energy.
theorem
CKN.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₀ ρ))
A local H¹ velocity slice has Euclidean norm in L³ on an interior ball.
The proof obtains L⁶ from the same-ball weak Sobolev estimate and lowers the
exponent on the finite-measure ball.
theorem
CKN.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 ρ))
For almost every time in a cylinder, the velocity has spatial L³ norm on
the cylinder's ball.
theorem
CKN.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)
A spatial L³ velocity slice gives global L^{3/2} and compact support
for each cut-off tensor entry. The summed source norm is bounded by the tensor
energy with the dimension factor included.
theorem
CKN.pressureUTensor_source_data_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}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), (∀ (i j : Fin 3),
MeasureTheory.MemLp
(fun (x : Vec 3) =>
mollifiedBallCutoff z.1 hρ x * pressureUTensor u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
(x, s) i j)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume) ∧ (∀ (i j : Fin 3),
HasCompactSupport fun (x : Vec 3) =>
mollifiedBallCutoff z.1 hρ x * pressureUTensor u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
(x, s) i j) ∧ ∑ i : Fin 3,
∑ j : Fin 3,
MeasureTheory.lpNorm
(fun (x : Vec 3) =>
mollifiedBallCutoff z.1 hρ x * pressureUTensor u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
(x, s) i j)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ (27 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, pressureUTensorNorm u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
s y ^ (3 / 2)) ^ (2 / 3)
The suitable-solution source package on almost every time slice of a cylinder, in the component-sum form used by the unconditional endpoint.