OAI/Analysis/CircleDomains/Transfer/RetainedSmallTests.lean

GitHub source file

1 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. theorem OAI.CircleDomainRigidity.SelectedMixedModels.small_anchored_of_retained_tests_at line 27