OAI/Analysis/CircleDomains/Selection/FiniteChainPotential.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The finite-chain infimum used in the compatible barrier construction. Costs may be infinite. In particular, truncation remains valid on components unreachable by finite-cost chains.

  1. inductive OAI.CircleDomainRigidity.PaidChain line 19
  2. theorem OAI.CircleDomainRigidity.PaidChain.single line 28
  3. theorem OAI.CircleDomainRigidity.PaidChain.append line 31
  4. theorem OAI.CircleDomainRigidity.PaidChain.reverse line 37
  5. def OAI.CircleDomainRigidity.chainDistance line 46
  6. theorem OAI.CircleDomainRigidity.chainDistance_le line 49
  7. theorem OAI.CircleDomainRigidity.chainDistance_anchor line 53
  8. theorem OAI.CircleDomainRigidity.le_chainDistance line 57
  9. theorem OAI.CircleDomainRigidity.chainDistance_extend line 61
  10. def OAI.CircleDomainRigidity.chainPotential line 69
  11. theorem OAI.CircleDomainRigidity.chainPotential_le_one line 71
  12. theorem OAI.CircleDomainRigidity.chainPotential_anchor line 73
  13. theorem OAI.CircleDomainRigidity.chainPotential_separated line 76
  14. theorem OAI.CircleDomainRigidity.min_one_add_le line 84
  15. theorem OAI.CircleDomainRigidity.chainPotential_extend line 91
  16. theorem OAI.CircleDomainRigidity.chainPotential_two_sided line 97