OAI/Analysis/CircleDomains/Selection/MeanMarkedBranchBands.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The chosen chart is retained together with each marked interval. This lets the same branch supply both the graph incidence interval and the physical terminal staircase estimate.

  1. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.exists_marked_branch_band line 20
  2. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.exists_marked_branch_band_family line 84