OAI/Analysis/CircleDomains/Selection/TrackedTailSequence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Track a scalar from any saved stage, with cumulative uniform and Sobolev-gradient errors controlled by the actual later budgets.

  1. def OAI.CircleDomainRigidity.AppendingSequence.tailIndex line 20
  2. def OAI.CircleDomainRigidity.AppendingSequence.tailScalar line 27
  3. def OAI.CircleDomainRigidity.AppendingSequence.tailWitness line 30
  4. theorem OAI.CircleDomainRigidity.AppendingSequence.tail_step_uniform line 37
  5. theorem OAI.CircleDomainRigidity.AppendingSequence.tail_step_gradient line 41
  6. theorem OAI.CircleDomainRigidity.AppendingSequence.tail_uniform_error line 47
  7. theorem OAI.CircleDomainRigidity.AppendingSequence.tail_gradient_error line 58