OAI/Analysis/CircleDomains/Sobolev/PrincipalCircleAreaEstimate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The analytic remainder contributes vanishing signed area. All bounds here come from its actual values and first derivatives.

  1. def OAI.CircleDomainRigidity.principalAreaErrorBudget line 14
  2. theorem OAI.CircleDomainRigidity.principal_area_budget_le line 17
  3. theorem OAI.CircleDomainRigidity.principal_circle_decomposition line 38
  4. theorem OAI.CircleDomainRigidity.principal_circle_area_estimate line 56