OAI/Analysis/CircleDomains/Selection/NewJumpLevel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A concrete new finite jump level inside the safe region. Its mesh may be made arbitrarily small while retaining the old chain lower bound minus the prescribed loss. Every new jump has positive toll and a domain boundary.

  1. theorem OAI.CircleDomainRigidity.exists_safe_new_jump_level line 22