Good points for the endpoint regularity argument

The domains and energy in this file use the spatial and parabolic conventions of def:good-point.

def ESS.goodPointPastCylinder (x : CKN.Foundation.Parabolic.Vec3) (t r : ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

The open space-time cylinder used in def:good-point.

Equations

• ESS.goodPointPastCylinder x t r = CKN.Foundation.Parabolic.vec3Ball x r ×ˢ Set.Ioo (t - r ^ 2) t

def ESS.goodPointDomain : Set CKN.Foundation.Parabolic.ParabolicPoint

The open domain and its closed top face used in def:good-point.

Equations

• ESS.goodPointDomain = CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0

def ESS.goodPointClosedTopDomain : Set CKN.Foundation.Parabolic.ParabolicPoint

The unit past cylinder including its top time slice.

Equations

• ESS.goodPointClosedTopDomain = CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioc (-1) 0

noncomputable def ESS.goodPointEnergy (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (x : CKN.Foundation.Parabolic.Vec3) (t r : ℝ) : ENNReal

The nonnegative velocity and pressure energy on a past cylinder. The CKN cylinder includes its top slice, which is null for space-time volume.

Equations

• One or more equations did not get rendered due to their size.

def ESS.IsGoodPoint (ε₀ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : Prop

A point is good when it has an admissible past cylinder with sufficiently small normalized velocity and pressure energy.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.goodPointEnergy_mono {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {x₁ x₂ : CKN.Foundation.Parabolic.Vec3} {t₁ t₂ r₁ r₂ : ℝ} (hsubset : CKN.Foundation.Parabolic.parabolicCylinder x₁ t₁ r₁ ⊆ CKN.Foundation.Parabolic.parabolicCylinder x₂ t₂ r₂) : goodPointEnergy u p x₁ t₁ r₁ ≤ goodPointEnergy u p x₂ t₂ r₂

The good-point energy is monotone in the cylinder.