OAI/Analysis/CircleDomains/Selection/SelectedRealSmallness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

At every unmarked end the actual selected family contains arbitrarily small anchored plateaus, with its real boundary-band norm.

  1. def OAI.CircleDomainRigidity.SmallAnchoredPlateaus line 20
  2. theorem OAI.CircleDomainRigidity.selected_real_family_smallness line 31