OAI/Analysis/CircleDomains/Selection/RecursiveTestHistory.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Every saved tolerance stays in the actual finite history. Thus each later test change is bounded by its geometric share of that tolerance.

  1. def OAI.CircleDomainRigidity.AppendingSequence.savedTolerance line 20
  2. theorem OAI.CircleDomainRigidity.AppendingSequence.savedTolerance_pos line 25
  3. theorem OAI.CircleDomainRigidity.AppendingSequence.history_mono line 28
  4. theorem OAI.CircleDomainRigidity.AppendingSequence.savedTolerance_mem line 37
  5. theorem OAI.CircleDomainRigidity.AppendingSequence.later_budget_le_saved line 40