OAI/Analysis/CircleDomains/Selection/MeanMarkedBands.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual interval representatives for the marked fibers of the mean period graph. At nonsingular marks their widths are bounded by the original path-hit probability, not by an assumed graph-width budget.

  1. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.exists_marked_band line 20
  2. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.exists_marked_band_family line 78