OAI/Analysis/CircleDomains/Modulus/ActualTwoEndedBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The common limiting budget for actual first-exit, middle, and last-entry restrictions of the original paths.

  1. def OAI.CircleDomainRigidity.middleFragment line 21
  2. theorem OAI.CircleDomainRigidity.actual_twoEnded_finite_budget line 26
  3. theorem OAI.CircleDomainRigidity.exists_actual_twoEnded_limits line 70