OAI/Analysis/CircleDomains/Modulus/RecursiveTailBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every finite tail spends less than one quarter of a previously saved tolerance. This controls both coordinates of each saved barrier.

  1. theorem OAI.CircleDomainRigidity.AppendingSequence.tail_budget_le_saved line 22