OAI/Analysis/CircleDomains/Selection/RecursiveTestConstruction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Iterate the constructed finite appending theorem, choosing each error below every saved tolerance in the finite history.

  1. structure OAI.CircleDomainRigidity.SavedAppendingStep line 13
  2. structure OAI.CircleDomainRigidity.AppendingConstructionState line 17
  3. def OAI.CircleDomainRigidity.AppendingConstructionState.chooseStep line 25
  4. def OAI.CircleDomainRigidity.AppendingConstructionState.next line 35
  5. def OAI.CircleDomainRigidity.appendingStates line 50
  6. theorem OAI.CircleDomainRigidity.appendingStates_history_length line 60
  7. theorem OAI.CircleDomainRigidity.appendingStates_family_count line 71