OAI/Analysis/CircleDomains/Selection/FiniteGapMultiplicity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An interval meeting at most one deleted hole can meet at most two retained gaps. This is the exact multiplicity in the tail-disk estimate.

  1. theorem OAI.CircleDomainRigidity.interval_meets_hole_between_gaps line 13
  2. theorem OAI.CircleDomainRigidity.at_most_two_gaps_of_at_most_one_hole line 32