Regularity at shifted cylinder centers

This file records the interior-neighborhood consequence of a Hölder representative on the shifted cylinder from lem:regular-point-shift.

theorem ESS.isRegularPoint_of_holder_on_shifted_cylinder (Ω : Set CKN.Foundation.Parabolic.Vec3) (I : Set ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ R γ : ℝ) (hR : 0 < R) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hAE : w =ᵐ[MeasureTheory.volume.restrict (goodPointPastCylinder x₀ (t₀ + R ^ 2 / 8) (R / 2))] u) (hγ : 0 < γ) (hγle : γ ≤ 1) (hHolder : CKN.ParabolicHolderVecOn (closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ (t₀ + R ^ 2 / 8) (R / 2))) w γ) (hclosure : closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ (t₀ + R ^ 2 / 8) (R / 2)) ⊆ CKN.spaceTimeSet Ω I) : CKN.IsRegularPoint Ω I u (x₀, t₀)

A Hölder representative on a shifted half-cylinder makes its interior center a CKN regular point.