OAI/Analysis/CircleDomains/Selection/JumpTollLowerBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A fixed positive neighborhood width pays the limiting dust junction. This is the lower bound used in removal of one shrinking jump level.

  1. def OAI.CircleDomainRigidity.fixedWidthJumpToll line 17
  2. theorem OAI.CircleDomainRigidity.eventually_mem_fixed_thickening line 21
  3. theorem OAI.CircleDomainRigidity.limiting_fixedWidthJumpToll_ge line 29
  4. theorem OAI.CircleDomainRigidity.fixedWidthJumpToll_ge_floor line 41