OAI/Analysis/CircleDomains/Modulus/FirstExitFragmentBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every finite collection of actual first-exit fragments eventually has cost at most the original path. Their limiting series has the same bound.

  1. theorem OAI.CircleDomainRigidity.firstExitFragmentArray_finite_budget line 20
  2. theorem OAI.CircleDomainRigidity.firstExitFragmentArray_limiting_budget line 52