OAI/Analysis/CircleDomains/Modulus/SmallMeanBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The small occupation and punctured hit norms used by compact arc reduction imply the quantitative strict Stokes budget needed for exclusion.

  1. def OAI.CircleDomainRigidity.meanBudgetConstant line 13
  2. def OAI.CircleDomainRigidity.meanBudgetTolerance line 16
  3. theorem OAI.CircleDomainRigidity.meanBudgetTolerance_pos line 19
  4. theorem OAI.CircleDomainRigidity.meanBudgetTolerance_ne_top line 26
  5. theorem OAI.CircleDomainRigidity.mean_budget_lt_of_small_norms line 29