OAI/Analysis/CircleDomains/Topology/RegularJordanCollarProof.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Construction of the precise regular Jordan inward collar from regular level charts and a compactly supported transverse field, using circle classification and the signed finite Green identity.

  1. lemma OAI.CircleDomainRigidity.exists_small_inward_field line 16
  2. theorem OAI.CircleDomainRigidity.smoothRegularJordanCollars line 61