Ess Local Proof Glue

Local endpoint regularity through vorticity estimates and backward uniqueness.

theorem ESS.essLocal_holder_of_all_good {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {ε₀ γ₀ : ℝ} (hγ₀ : 0 < γ₀) (hγ₀le : γ₀ ≤ 1) (hglue : ∀ {K : Set CKN.Foundation.Parabolic.ParabolicPoint}, IsCompact K → K ⊆ {z : CKN.Foundation.Parabolic.ParabolicPoint | CKN.Foundation.Parabolic.vec3EuclideanNorm (z.1 - 0) ≤ 1 / 2 ∧ z.2 ∈ Set.Icc (-(1 / 4)) 0} → (∀ z ∈ K, IsGoodPoint ε₀ u p z) → ∃ (N : Set CKN.Foundation.Parabolic.ParabolicPoint) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), K ⊆ N ∧ N ⊆ goodPointClosedTopDomain ∧ IsOpen {z : { q : CKN.Foundation.Parabolic.ParabolicPoint // q ∈ goodPointClosedTopDomain } | ↑z ∈ N} ∧ w =ᵐ[MeasureTheory.volume.restrict (N ∩ goodPointDomain)] u ∧ CKN.ParabolicHolderVecOn K w γ₀) (hgood : ∀ z ∈ closure (CKN.Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2)), IsGoodPoint ε₀ u p z) : ∃ (γ : ℝ), 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 γ

A common Hölder representative on the closed target cylinder restricts to the original velocity almost everywhere on the past cylinder.

theorem ESS.essLocal_suitable_of_localEnergyEqualities {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 → ℝ} (hdata : CKN.IsSuitableWeakSolutionData (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) 3 u Du p 0) (hdiv : ∀ ψ ∈ 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) (hmom : ∀ φ ∈ 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) (henergy : ∀ (r : ℝ), 0 < r → r < 1 → ∀ ψ ∈ 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 1) (Set.Ioo (-1) 0) 3 u Du p 0

Local energy equalities on all smaller concentric cylinders assemble into the local energy inequality on the unit cylinder. Compact support keeps each test inside one such smaller cylinder.

theorem ESS.essLocal_suitableData_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)))) (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) : CKN.IsSuitableWeakSolutionData (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) 3 u Du p 0

The hypotheses of thm:ess-local supply the local data clauses of CKN suitability on the full open unit cylinder.