OAI/Analysis/CircleDomains/Modulus/ActualOneEndedBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual retained prefixes and final fragments, with one common subsequence and the correct one-ended limiting budget.

  1. def OAI.CircleDomainRigidity.prefixFragment line 21
  2. theorem OAI.CircleDomainRigidity.actual_oneEnded_finite_budget line 26
  3. theorem OAI.CircleDomainRigidity.exists_actual_oneEnded_limits line 57