OAI/Analysis/CircleDomains/Selection/SelectedMixedSmallness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The real seed's collapse estimates survive the common mixed construction, even when its real coordinates are enumerated differently and further marked points are retained.

  1. def OAI.CircleDomainRigidity.SelectedMixedModels.realCoordinates line 27
  2. def OAI.CircleDomainRigidity.SelectedMixedModels.withRadius line 32
  3. theorem OAI.CircleDomainRigidity.SelectedMixedModels.retains_real_presentation line 37
  4. theorem OAI.CircleDomainRigidity.SelectedMixedModels.small_anchored_of_retained_tests line 45