Relative neighborhoods of good points

This file proves the openness and local representative parts of lem:good-open-glue.

theorem ESS.goodPoint_closedTop_subset_closure_domain : goodPointClosedTopDomain ⊆ closure goodPointDomain

The closed top domain lies in the closure of the open space-time domain. This lets a relatively open intersection with the top face be tested from below in time.

theorem ESS.goodPoint_local_holder_patch {ε₀ γ₀ C₄ : ℝ} (hC₄ : 0 ≤ C₄) (hTop : ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ ρ r : ℝ) (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 → ℝ), 0 < r → r < ρ → (CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball x₀ ρ) (Set.Ioo (t₀ - ρ ^ 2) t₀) 3 u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) → ENNReal.ofReal (r⁻¹ ^ 2) * goodPointEnergy u p x₀ t₀ r < ENNReal.ofReal (ε₀ / 8) → ∃ (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (goodPointPastCylinder x₀ t₀ (r / 2))] u ∧ (∀ z ∈ closure (goodPointPastCylinder x₀ t₀ (r / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ 2 * C₄ * r⁻¹) ∧ ∀ z ∈ closure (goodPointPastCylinder x₀ t₀ (r / 2)), ∀ z' ∈ closure (goodPointPastCylinder x₀ t₀ (r / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z - w z') ≤ 4 * C₄ * r⁻¹ * (8 * r⁻¹) ^ γ₀ * CKN.Foundation.Parabolic.parabolicDist z z' ^ γ₀) {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 → ℝ} (hSuitable : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) 3 u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ goodPointClosedTopDomain) (hgood : IsGoodPoint ε₀ u p z) : ∃ (δ : ℝ) (Cpatch : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), 0 < δ ∧ 0 ≤ Cpatch ∧ w =ᵐ[MeasureTheory.volume.restrict (Metric.ball z δ ∩ goodPointDomain)] u ∧ CKN.ParabolicHolderVecNormLE (Metric.ball z δ ∩ goodPointDomain) w γ₀ Cpatch ∧ CKN.ParabolicHolderVecNormLE (Metric.ball z δ ∩ goodPointClosedTopDomain) w γ₀ Cpatch

A good point has a local representative with Hölder bounds on both the open past and the closed top portion of its neighborhood.

theorem ESS.goodPoint_set_relative_open {ε₀ : ℝ} {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 → ℝ} (hSuitable : 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}

Good points form a relatively open subset of the closed top domain.