Ess Local Proof

Local endpoint regularity through vorticity estimates and backward uniqueness.

theorem ESS.essLocal_of_inputs {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)))) (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) (hBlowup : ∀ (ε₀ : ℝ), 0 < ε₀ → ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ), x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2)) → t₀ ∈ Set.Icc (-(1 / 4)) 0 → ¬IsGoodPoint ε₀ u p (x₀, t₀) → (∀ (k : ℕ), 0 < r k) → Filter.Tendsto r Filter.atTop (nhds 0) → ∃ (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), Measurable U ∧ (∀ (R a : ℝ), 0 < R → a < 0 → CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo a 0) 3 U DU q 0) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-2) 0), ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t) i) fun (x : CKN.Foundation.Parabolic.Vec3) => DU (x, t) i) ∧ (∀ (T : ℝ), 0 < T → essSup (fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (U (x, t))) 3 MeasureTheory.volume) (MeasureTheory.volume.restrict (Set.Ioo (-T) 0)) < ⊤) ∧ (∀ (T : ℝ), 0 < T → MeasureTheory.MemLp q (3 / 2) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (-T) 0)))) ∧ HasZeroDistributionalVelocityTrace U ∧ (U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (-2) 0))] 0 → Filter.Tendsto (fun (k : ℕ) => goodPointEnergy (blowupVelocity x₀ t₀ (r k) u) (blowupPressure x₀ t₀ (r k) p) 0 0 1) Filter.atTop (nhds 0))) : ∃ (γ : ℝ), 0 < γ ∧ γ ≤ 1 ∧ ∃ (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ CKN.ParabolicHolderVecOn (closure (CKN.Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ

The local Escauriaza–Seregin–Šverák regularity conclusion from its local weak-solution hypotheses.