Local Energy Limit #
Local energy identities and limit passages for the endpoint regularity proof.
theorem
ESS.localEnergyLimitHolderTripleFourFourFourThirds :
ENNReal.HolderTriple 2 4 (ENNReal.ofReal (4 / 3))
theorem
ESS.localEnergyLimitHolderTripleFourThirdsFourOne :
(ENNReal.ofReal (4 / 3)).HolderTriple 4 1
theorem
ESS.localEnergyLimitHolderTripleThreeHalvesFourTwelveElevenths :
(ENNReal.ofReal (3 / 2)).HolderTriple 4 (ENNReal.ofReal (12 / 11))
theorem
ESS.localEnergyLimitHolderTripleTwelveEleventhsTwelveOne :
(ENNReal.ofReal (12 / 11)).HolderTriple 12 1
theorem
ESS.localEnergy_mollifiedBase_integral_limit_zero
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hu :
MeasureTheory.AEStronglyMeasurable u
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hDu :
MeasureTheory.AEStronglyMeasurable Du
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(henergy :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤)
(hpLp :
MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤)
(hgrad :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (i : Fin 3),
CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 1) (fun (x : CKN.Vec 3) => u (x, t) i)
fun (x : CKN.Vec 3) => Du (x, t) i)
(hS2 :
∀ ψ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z = 0)
(hS3 :
∀ φ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3,
∑ j : Fin 3,
u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3,
∑ j : Fin 3,
Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0)
{ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
(hψU : tsupport ψ ⊆ localEnergyUnitProductCylinder)
:
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), localEnergyLimitExpandedBaseIntegrand
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) (i : Fin 3) => localEnergyVelocityZeroExtension u i z)
(fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => 0)
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) => localEnergyGradientZeroExtension Du i j z)
(localEnergyPressureZeroExtension p)
(have this := ψ;
this)
z = 0
The zero-extended local energy density has zero integral for each smooth test supported strictly inside the unit cylinder.