Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.LocalEnergyResult

Local Energy Result #

Local energy identities and limit passages for the endpoint regularity proof.

source
noncomputable def ESS.localEnergyIdentityDensityProduct (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 → ℝ) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) :
CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The product-coordinate form of the local energy identity density.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ESS.localEnergyIdentity_of_essLocalData {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 → ℝ} {r : ℝ} (hr1 : r < 1) (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)))) (hp : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hL2 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ‖u (x, t)‖ₑ ^ 2) (MeasureTheory.volume.restrict (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 - ∑ i : Fin 3, 0 z i * φ z i = 0) {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo (-1) 0)) :
    2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo (-1) 0), CKN.spatialGradientSq u Du z * ψ z = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo (-1) 0), CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (CKN.timePartial ψ z + ∑ i : Fin 3, CKN.spatialSecondPartial ψ i i z) + (CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 + 2 * p z) * ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z

    The energy equality on a smaller cylinder, obtained as the limit of the space-time mollified local energy identities.

    source
    theorem ESS.leiL4_of_essLocalData {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 → ℝ} {r : ℝ} (hr0 : 0 < r) (hr1 : r < 1) (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)))) (hp : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hL2 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ‖u (x, t)‖ₑ ^ 2) (MeasureTheory.volume.restrict (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 - ∑ i : Fin 3, 0 z i * φ z i = 0) :
    MeasureTheory.MemLp u 4 (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo (-1) 0))) ∧ (∀ ψ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo (-1) 0), 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo (-1) 0), CKN.spatialGradientSq u Du z * ψ z = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo (-1) 0), CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (CKN.timePartial ψ z + ∑ i : Fin 3, CKN.spatialSecondPartial ψ i i z) + (CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 + 2 * p z) * ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z) ∧ CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo (-1) 0) 3 u Du p 0

    The conclusion of lem:lei-L4: local space-time L⁴ regularity, local energy equality, and suitability on every smaller cylinder.