RegularJordanCollar.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth inward collars for regular Jordan boundaries.

Published input: J. M. Lee, Introduction to Smooth Manifolds, second edition (2013), Theorem 9.25, pp.222--223 (Collar Neighborhood Theorem), together with its regular-domain interpretation in Proposition5.47, p.121. The formulation below is the compact planar Jordan-boundary specialization: parametrize the boundary circle (Milnor's compact one-manifold classification), take inward collar slices, and use their bounded Jordan sides (planar Schoenflies). It is a specialization/corollary, not a verbatim transcription of Theorem9.25. The continuous-tangent clause retains the C¹ dependence of its smooth collar embedding and is used only for the uniform boundary variation bound. The regular-level hypothesis is retained explicitly. https://thunv.wordpress.com/wp-content/uploads/2015/09/graduate-texts-in-mathematics-vol-218-john-m-lee-introduction-to-smooth-manifolds-springer-2013.pdf DOI: 10.1007/978-1-4419-9982-5.

structure OAI.CircleDomainRigidity.RegularJordanInwardCollar line 29
def OAI.CircleDomainRigidity.SmoothRegularJordanCollars line 45
Source documentation
Explicit published-input parameter: the regular-level planar Jordan specialization of the collar-neighborhood theorem described above.
```
def SmoothRegularJordanCollars : Prop :=
…
```
theorem OAI.CircleDomainRigidity.WeightedCollar.exists_regular_inward_collar line 50
theorem OAI.CircleDomainRigidity.RegularJordanInwardCollar.uniform_approach line 56
theorem OAI.CircleDomainRigidity.RegularJordanInwardCollar.eventually_in_boundary_neighborhood line 77