The next result is the time integration of the slice estimate. Its time-energy hypothesis is exactly the sliced form of the space-time L² energy bound and is derived from that bound in the E1 wrapper.
theorem
CKN.eLpNorm_three_pow_eq_lintegral
{α E : Type}
[MeasurableSpace α]
[TopologicalSpace E]
[ContinuousENorm E]
{μ : MeasureTheory.Measure α}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
The cube of the L³ seminorm is the integral of the cubed extended norm.
theorem
CKN.scalarTimeL2Energy_eq
{E : Type}
[TopologicalSpace E]
[ContinuousENorm E]
{J : Set ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{r : ℝ}
(f : Foundation.Parabolic.Vec3 × ℝ → E)
(hf :
MeasureTheory.AEStronglyMeasurable f
((MeasureTheory.volume.restrict (euclideanBall x₀ r)).prod (MeasureTheory.volume.restrict J)))
:
∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2
(MeasureTheory.volume.restrict (euclideanBall x₀ r)) ^ 2 = ∫⁻ (z : Vec 3 × ℝ), ‖f z‖ₑ ^ 2 ∂(MeasureTheory.volume.restrict (euclideanBall x₀ r)).prod (MeasureTheory.volume.restrict J)
Tonelli identifies the time integral of the squared spatial L² norm with the space-time squared norm.
theorem
CKN.scalarSliceL4_bound_ae
{x₀ : Foundation.Parabolic.Vec3}
{r : ℝ}
{J : Set ℝ}
(hr : 0 < r)
(f : Foundation.Parabolic.Vec3 × ℝ → ℝ)
(g : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3)
{A : ENNReal}
(hA : A < ⊤)
(h3 :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 3
(MeasureTheory.volume.restrict (euclideanBall x₀ r)) ≤ A)
(hSlice :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (v : H1Function (euclideanBall x₀ r)),
(fun (x : Foundation.Parabolic.Vec3) => f (x, t)) =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ r)] v.toFun ∧ (fun (x : Foundation.Parabolic.Vec3) => g (x, t)) =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ r)] v.grad)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 4
(MeasureTheory.volume.restrict (euclideanBall x₀ r)) ∧ MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 4
(MeasureTheory.volume.restrict (euclideanBall x₀ r)) ^ 4 ≤ A ^ 2 * (ENNReal.ofReal sobolevPoincareFaithfulC5 * (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => g (x, t)) 2
(MeasureTheory.volume.restrict (euclideanBall x₀ r)) + (ENNReal.ofReal r)⁻¹ * MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2
(MeasureTheory.volume.restrict (euclideanBall x₀ r)))) ^ 2
Almost every H¹ slice with a uniform L³ bound obeys the quantitative L⁴ interpolation
estimate used in lem:lei-L4 of the Escauriaza–Seregin–Šverák manuscript.
theorem
CKN.scalarCylinderL4_of_sliceBounds
{x₀ : Foundation.Parabolic.Vec3}
{r : ℝ}
{J : Set ℝ}
(hr : 0 < r)
(f : Foundation.Parabolic.Vec3 × ℝ → ℝ)
(g : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3)
(hf :
MeasureTheory.AEStronglyMeasurable f
((MeasureTheory.volume.restrict (euclideanBall x₀ r)).prod (MeasureTheory.volume.restrict J)))
(hA :
essSup
(fun (t : ℝ) =>
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 3
(MeasureTheory.volume.restrict (euclideanBall x₀ r)))
(MeasureTheory.volume.restrict J) < ⊤)
(henergy :
∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2
(MeasureTheory.volume.restrict (euclideanBall x₀ r)) ^ 2 + MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => g (x, t)) 2
(MeasureTheory.volume.restrict (euclideanBall x₀ r)) ^ 2 < ⊤)
(hSlice :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (v : H1Function (euclideanBall x₀ r)),
(fun (x : Foundation.Parabolic.Vec3) => f (x, t)) =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ r)] v.toFun ∧ (fun (x : Foundation.Parabolic.Vec3) => g (x, t)) =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ r)] v.grad)
:
MeasureTheory.MemLp f 4 ((MeasureTheory.volume.restrict (euclideanBall x₀ r)).prod (MeasureTheory.volume.restrict J))
A uniform spatial L³ bound and finite time-integrated L² energy imply the cylinder L⁴ bound.
theorem
CKN.scalarCylinderL4_of_jointEnergy
{x₀ : Foundation.Parabolic.Vec3}
{r : ℝ}
{J : Set ℝ}
(hr : 0 < r)
(f : Foundation.Parabolic.Vec3 × ℝ → ℝ)
(g : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3)
(hf :
MeasureTheory.AEStronglyMeasurable f
((MeasureTheory.volume.restrict (euclideanBall x₀ r)).prod (MeasureTheory.volume.restrict J)))
(hg :
MeasureTheory.AEStronglyMeasurable g
((MeasureTheory.volume.restrict (euclideanBall x₀ r)).prod (MeasureTheory.volume.restrict J)))
(hA :
essSup
(fun (t : ℝ) =>
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 3
(MeasureTheory.volume.restrict (euclideanBall x₀ r)))
(MeasureTheory.volume.restrict J) < ⊤)
(henergy :
∫⁻ (z : Vec 3 × ℝ), ‖f z‖ₑ ^ 2 + ‖g z‖ₑ ^ 2 ∂(MeasureTheory.volume.restrict (euclideanBall x₀ r)).prod (MeasureTheory.volume.restrict J) < ⊤)
(hSlice :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (v : H1Function (euclideanBall x₀ r)),
(fun (x : Foundation.Parabolic.Vec3) => f (x, t)) =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ r)] v.toFun ∧ (fun (x : Foundation.Parabolic.Vec3) => g (x, t)) =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ r)] v.grad)
:
MeasureTheory.MemLp f 4 ((MeasureTheory.volume.restrict (euclideanBall x₀ r)).prod (MeasureTheory.volume.restrict J))
The cylinder estimate needs only the local space-time L² energy: Tonelli turns it into the
time-integrated slice energy used by scalarCylinderL4_of_sliceBounds.
The E1 cylinder estimate #
theorem
CKN.velocityComponent_memLp_four_of_essLocalData
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{i : Fin 3}
{r : ℝ}
(hr : 0 < r)
(hr1 : r ≤ 1)
(hu :
MeasureTheory.AEStronglyMeasurable u
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hDu :
MeasureTheory.AEStronglyMeasurable Du
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(henergy :
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤)
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤)
(hgrad :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (j : Fin 3),
HasWeakGradientOn (Foundation.Parabolic.vec3Ball 0 1) (fun (x : Vec 3) => u (x, t) j) fun (x : Vec 3) =>
Du (x, t) j)
:
MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) 4
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo (-1) 0)))
Each velocity component is in space-time L⁴ on a smaller ball cylinder under the
energy, L∞ₜL³ₓ, and slice-gradient hypotheses of thm:ess-local of the
Escauriaza–Seregin–Šverák manuscript.
theorem
CKN.velocity_memLp_four_of_essLocalData
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{r : ℝ}
(hr : 0 < r)
(hr1 : r ≤ 1)
(hu :
MeasureTheory.AEStronglyMeasurable u
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hDu :
MeasureTheory.AEStronglyMeasurable Du
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(henergy :
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤)
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤)
(hgrad :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (j : Fin 3),
HasWeakGradientOn (Foundation.Parabolic.vec3Ball 0 1) (fun (x : Vec 3) => u (x, t) j) fun (x : Vec 3) =>
Du (x, t) j)
:
MeasureTheory.MemLp u 4
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo (-1) 0)))
The vector velocity has space-time L⁴ on every smaller ball cylinder under the
energy, L∞ₜL³ₓ, and slice-gradient hypotheses of thm:ess-local (ESS).
theorem
CKN.velocity_memLp_four_unit_of_essLocalData
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
(hu :
MeasureTheory.AEStronglyMeasurable u
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hDu :
MeasureTheory.AEStronglyMeasurable Du
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(henergy :
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤)
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤)
(hgrad :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (j : Fin 3),
HasWeakGradientOn (Foundation.Parabolic.vec3Ball 0 1) (fun (x : Vec 3) => u (x, t) j) fun (x : Vec 3) =>
Du (x, t) j)
:
MeasureTheory.MemLp u 4
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))
The velocity has space-time L⁴ on the full unit cylinder under the hypotheses of
thm:ess-local (ESS).