OAI/Analysis/CircleDomains/Uniformization/TrackedTestLimits.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual old coordinates have continuous sphere limits and strong L2 gradient limits. Both stay within the total recursive error budget.

  1. def OAI.CircleDomainRigidity.AppendingSequence.sphereScalar line 27
  2. theorem OAI.CircleDomainRigidity.AppendingSequence.exists_continuous_limit line 32
  3. theorem OAI.CircleDomainRigidity.AppendingSequence.exists_gradient_limit line 58