Compact gluing of good-point representatives #
This file proves the compact-set and bad-point conclusions of
lem:good-open-glue.
theorem
ESS.goodPoint_badPoint_lower_bound_closed
{ε₀ : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{z : CKN.Foundation.Parabolic.ParabolicPoint}
{R : ℝ}
(hz : CKN.Foundation.Parabolic.vec3EuclideanNorm (z.1 - 0) ≤ 1 / 2 ∧ z.2 ∈ Set.Icc (-(1 / 4)) 0)
(hRpos : 0 < R)
(hRdomain : goodPointPastCylinder z.1 z.2 R ⊆ goodPointDomain)
(hnot : ¬IsGoodPoint ε₀ u p z)
:
A point in the closed compact region which is not good satisfies the
lower bound in eq:bad-point-lower-bound at every admissible radius.
theorem
ESS.goodPoint_open_glue :
∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ),
0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ (∀ {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 → ℝ},
(CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) 3 u Du p
fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) →
IsOpen
{z : { q : CKN.Foundation.Parabolic.ParabolicPoint // q ∈ goodPointClosedTopDomain } | IsGoodPoint ε₀ u p ↑z} ∧ ∀ {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 γ₀) ∧ ∀ {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} {R : ℝ},
CKN.Foundation.Parabolic.vec3EuclideanNorm (z.1 - 0) ≤ 1 / 2 →
z.2 ∈ Set.Icc (-(1 / 4)) 0 →
0 < R →
goodPointPastCylinder z.1 z.2 R ⊆ goodPointDomain →
¬IsGoodPoint ε₀ u p z →
ENNReal.ofReal (R⁻¹ ^ 2) * goodPointEnergy u p z.1 z.2 R ≥ ENNReal.ofReal (ε₀ / 8)
Good points are relatively open, and every compact subset of good points
has one representative which is Hölder on the entire compact set, including
its top-face points. The same constants also give the bad-point lower bound
in eq:bad-point-lower-bound.