OAI/Analysis/CircleDomains/Probability/CenteredArcLaw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transport of the constructed terminal arc law to centered disk coordinates. The coordinate extension is only evaluated on the closed collar.

  1. lemma OAI.CircleDomainRigidity.terminalArcSet_mapsTo_closure line 19
  2. def OAI.CircleDomainRigidity.diskTerminalArcSet line 30
  3. theorem OAI.CircleDomainRigidity.centeredJordanPath_mem line 34
  4. def OAI.CircleDomainRigidity.centeredArcLaw line 60
  5. theorem OAI.CircleDomainRigidity.centeredArcLaw_hit line 63
  6. theorem OAI.CircleDomainRigidity.exists_centered_compact_arc_law line 87