OAI/Analysis/CircleDomains/Modulus/BarrierErrorBudgets.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Choose the finite numerical budgets in the order required by the near-extremal model construction. No analytic conclusion is assumed.

  1. theorem OAI.CircleDomainRigidity.exists_barrier_error_budget line 12
  2. theorem OAI.CircleDomainRigidity.exists_height_error_scale line 25