OAI/Analysis/CircleDomains/Selection/TrackedTestSequence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Follow each old scalar through every actual appending stage. The coordinate indices shift by two, and both errors retain the chosen budget.

  1. def OAI.CircleDomainRigidity.AppendingSequence.index line 21
  2. def OAI.CircleDomainRigidity.AppendingSequence.scalar line 27
  3. def OAI.CircleDomainRigidity.AppendingSequence.witness line 30
  4. theorem OAI.CircleDomainRigidity.AppendingSequence.step_uniform line 37
  5. theorem OAI.CircleDomainRigidity.AppendingSequence.step_gradient line 41
  6. theorem OAI.CircleDomainRigidity.AppendingSequence.scalar_continuous line 46
  7. theorem OAI.CircleDomainRigidity.AppendingSequence.scalar_compact line 49