Good-point neighborhoods and gluing #
This file proves the lower bound at bad points and the local gluing statement from lem:good-open-glue.
theorem
ESS.exists_smaller_radius_preserving_goodPoint_smallness
{E : ENNReal}
{r ε : ℝ}
(hr : 0 < r)
(hsmall : ENNReal.ofReal (r⁻¹ ^ 2) * E < ENNReal.ofReal (ε / 8))
:
A strict good-point energy bound persists at some smaller positive radius.
This is the radius choice used in lem:good-open-glue.
theorem
ESS.goodPoint_smaller_radius_admissible
{z : CKN.Foundation.Parabolic.ParabolicPoint}
{R r : ℝ}
(hz : z ∈ goodPointClosedTopDomain)
(hRpos : 0 < R)
(hrpos : 0 < r)
(hrR : r < R)
(hRdomain : goodPointPastCylinder z.1 z.2 R ⊆ goodPointDomain)
:
goodPointPastCylinder z.1 z.2 r ⊆ goodPointDomain ∧ closure (CKN.Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ goodPointClosedTopDomain
A smaller past cylinder and its closure remain in the closed top domain.
This is the admissibility step used in lem:good-open-glue.