OAI/Analysis/CircleDomains/Modulus/StokesBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite Stokes estimate with distinct terminal labels and the actual positive-excess budget. The second theorem performs the diagonal limit; its hypotheses are the numerical estimates proved by finite transfer and Stokes.

  1. theorem OAI.CircleDomainRigidity.circle_stokes_bound_of_excess line 17
  2. theorem OAI.CircleDomainRigidity.stokes_limsup_of_vanishing_errors line 35