OAI/Analysis/CircleDomains/Modulus/RecursiveLimitBarriers.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Diagonal selection of actual finite-model barriers around a matched limit end. The only small-energy data used are the saved recursive pairs.

  1. theorem OAI.CircleDomainRigidity.AppendingSequence.saved_model_barrier_of_le line 23
  2. theorem OAI.CircleDomainRigidity.AppendingSequence.saved_barrier_around_matched_end line 35