OAI/Analysis/CircleDomains/Selection/SeededMixedSmallness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The first selection's small real tests retain their collapse estimates through every later mixed selection, using the original presentations at the seed labels.

  1. theorem OAI.CircleDomainRigidity.seeded_mixed_small_anchored line 17