OAI/Analysis/CircleDomains/Selection/PeriodBandGraph.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The period-coordinate level graph of Definition 2.3, assembled from local real branches on the punctured mask. The singular point belongs to every level. Integer changes of sheet give the compatibility used below; the closedness proof only needs the resulting equality of projected bands.

  1. def OAI.CircleDomainRigidity.periodBandGraph line 18
  2. theorem OAI.CircleDomainRigidity.periodBandGraph_on_patch line 22
  3. theorem OAI.CircleDomainRigidity.isClosed_periodBandGraph line 36
  4. theorem OAI.CircleDomainRigidity.periodBandGraph_singular line 63
  5. theorem OAI.CircleDomainRigidity.periodBandGraph_subset_mask line 68
  6. theorem OAI.CircleDomainRigidity.periodBandGraph_fiber_on_patch line 73
  7. theorem OAI.CircleDomainRigidity.isClosed_periodBandGraph_of_integer_transitions line 86