OAI/Analysis/CircleDomains/Modulus/BarrierJumpLosses.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A fixed summable loss schedule for the compatible-barrier chain distance. Its retained lower bound stays strictly above one quarter at every stage.

  1. def OAI.CircleDomainRigidity.barrierStageLower line 12
  2. def OAI.CircleDomainRigidity.barrierStageLoss line 14
  3. theorem OAI.CircleDomainRigidity.barrierStageLower_zero line 16
  4. theorem OAI.CircleDomainRigidity.barrierStageLower_sub_loss line 19
  5. theorem OAI.CircleDomainRigidity.barrierStageLoss_pos line 24
  6. theorem OAI.CircleDomainRigidity.barrierStageLoss_lt line 28
  7. theorem OAI.CircleDomainRigidity.quarter_lt_barrierStageLower line 33