Ess Local Proof Liouville

Local endpoint regularity through vorticity estimates and backward uniqueness.

theorem ESS.essLocal_slices_memLp_of_euclidean_essSup (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hU : Measurable U) (J : Set ℝ) (hbound : essSup (fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (U (x, t))) 3 MeasureTheory.volume) (MeasureTheory.volume.restrict J) < ⊤) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t)) 3 MeasureTheory.volume

A uniform essential bound for Euclidean slice norms gives ordinary L³ membership on almost every time slice.

theorem ESS.essLocal_slices_divergenceFree_of_local_suitable (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 → ℝ) (hsol : ∀ (R a : ℝ), 0 < R → a < 0 → CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo a 0) 3 U DU q 0) (hL3 : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-2) 0), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t)) 3 MeasureTheory.volume) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-2) 0), CKN.DistributionalDivergenceFree fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t)

Suitability on every bounded past cylinder makes almost every global spatial slice divergence free.

theorem ESS.essLocal_slices_curlFree_of_zero_vorticity (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hL3 : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-2) 0), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t)) 3 MeasureTheory.volume) (hgrad : ∀ᵐ (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) (hzero : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-2) 0), (fun (x : CKN.Foundation.Parabolic.Vec3) => weakVorticity DU (x, t)) =ᵐ[MeasureTheory.volume] 0) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-2) 0), ∀ (i j : Fin 3) (φ : CKN.Foundation.Parabolic.Vec3 → ℝ), CKN.SmoothCompactTest φ → ∫ (x : CKN.Foundation.Parabolic.Vec3), U (x, t) i * CKN.spatialDeriv φ j x - U (x, t) j * CKN.spatialDeriv φ i x = 0

A zero weak vorticity and the slice weak-gradient identity imply the distributional curl condition used by liouvilleL3.

theorem ESS.essLocal_limit_zero_of_slicewise_div_curl (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hU : Measurable U) (hslices : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-2) 0), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t)) (ENNReal.ofReal 3) MeasureTheory.volume ∧ (CKN.DistributionalDivergenceFree fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t)) ∧ ∀ (i j : Fin 3) (φ : CKN.Foundation.Parabolic.Vec3 → ℝ), CKN.SmoothCompactTest φ → ∫ (x : CKN.Foundation.Parabolic.Vec3), U (x, t) i * CKN.spatialDeriv φ j x - U (x, t) j * CKN.spatialDeriv φ i x = 0) : U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (-2) 0))] 0

Divergence-free and curl-free critical slices make the ancient velocity vanish on the final two time units.