Ess Local Proof Exterior

Local endpoint regularity through vorticity estimates and backward uniqueness.

theorem ESS.essLocal_matrixGradientEnergy_le_spatialGradientEnergy (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (x : CKN.Foundation.Parabolic.Vec3) (t r E : ℝ) (hbound : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder x t r, ENNReal.ofReal (CKN.spatialGradientSq U DU z) ≤ ENNReal.ofReal (E ^ 2)) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder x t r, ‖DU z‖ₑ ^ 2 ≤ ENNReal.ofReal (E ^ 2)

The matrix-valued weak-gradient norm is controlled by the scalar Dirichlet density used in the suitable-solution energy inequality.

theorem ESS.essLocal_uniformGradientEnergy_of_globalMass (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 : CKN.IsSuitableWeakSolutionIntegrable Set.univ (Set.Ioo (-12) 0) 3 U DU q 0) (hUmass : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo (-12) 0), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (U z)) ^ 3 < ⊤) (hqmass : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo (-12) 0), ENNReal.ofReal |q z| ^ (3 / 2) < ⊤) : ∃ (E : ℝ), 0 ≤ E ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3), ∀ t ∈ Set.Ioo (-2) 0, ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder x t 1, ‖DU z‖ₑ ^ 2 ≤ ENNReal.ofReal (E ^ 2)

Global critical velocity and pressure masses give one local Dirichlet bound on every unit past cylinder whose top lies in (-2,0).

theorem ESS.essLocal_globalVelocity_memLp_three (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hU : Measurable U) (J : Set ℝ) (hJ : MeasureTheory.volume J < ⊤) (hL3 : 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) < ⊤) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Parabolic.vec3EuclideanNorm (U (z.1, z.2))) 3 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict J))

A finite essential supremum of the spatial L³ norm gives space-time L³ membership on every finite time interval.

theorem ESS.essLocal_exterior_lintegral_tendsto_zero (F : CKN.Foundation.Parabolic.Vec3 × ℝ → ENNReal) (J : Set ℝ) (hF : AEMeasurable F (MeasureTheory.volume.prod (MeasureTheory.volume.restrict J))) (hFint : ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), F z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict J) ≠ ⊤) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in {z : CKN.Foundation.Parabolic.Vec3 × ℝ | ↑n < CKN.Foundation.Parabolic.vec3EuclideanNorm z.1}, F z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict J)) Filter.atTop (nhds 0)

The space-time integral of an integrable density outside expanding spatial balls tends to zero.

theorem ESS.essLocal_globalCriticalMasses_parabolic (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (J : Set ℝ) (hFtop : ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (U (z.1, z.2))) ^ 3 + ENNReal.ofReal |q (z.1, z.2)| ^ (3 / 2) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict J) < ⊤) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ J, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (U z)) ^ 3 < ⊤ ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ J, ENNReal.ofReal |q z| ^ (3 / 2) < ⊤

A finite product-coordinate critical energy gives separate finite velocity and pressure masses in CKN parabolic coordinates.

theorem ESS.essLocal_pressure_memLp_product (q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (J : Set ℝ) (hJ : MeasurableSet J) (hq : MeasureTheory.MemLp q (3 / 2) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ J))) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => q (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) (3 / 2) (MeasureTheory.volume.restrict (Set.univ ×ˢ J))

A pressure L^(3/2) bound on a whole-space past cylinder transfers to product coordinates.

theorem ESS.essLocal_globalCriticalEnergy_memLp (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hU : Measurable U) (J : Set ℝ) (hJ : MeasureTheory.volume J < ⊤) (hJmeas : MeasurableSet J) (hL3 : 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) < ⊤) (hq : MeasureTheory.MemLp q (3 / 2) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ J))) : ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (U (z.1, z.2))) ^ 3 + ENNReal.ofReal |q (z.1, z.2)| ^ (3 / 2) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict J) < ⊤

The velocity and pressure hypotheses in the blow-up projection make the critical energy density integrable on a finite past time interval.

theorem ESS.essLocal_exteriorCriticalTail (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hU : Measurable U) (J : Set ℝ) (hJ : MeasureTheory.volume J < ⊤) (hJmeas : MeasurableSet J) (hL3 : 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) < ⊤) (hq : MeasureTheory.MemLp q (3 / 2) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ J))) {ε : ENNReal} (hε : 0 < ε) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in {z : CKN.Foundation.Parabolic.Vec3 × ℝ | ↑n < CKN.Foundation.Parabolic.vec3EuclideanNorm z.1}, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (U (z.1, z.2))) ^ 3 + ENNReal.ofReal |q (z.1, z.2)| ^ (3 / 2) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict J) < ε

The critical velocity and pressure masses outside large spatial balls are uniformly small.

theorem ESS.essLocal_setIntegral_eq_productTimeRestriction (J : Set ℝ) (S : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)) (hS : S ⊆ Set.univ ×ˢ J) (F : CKN.Foundation.Parabolic.Vec3 × ℝ → ENNReal) : ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in S, F z = ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in S, F z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict J)

On a set whose times lie in J, integration against the product restriction agrees with integration against full space-time volume.