OAI/Analysis/CircleDomains/Sobolev/CoareaL2Errors.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Summable strong Sobolev errors vanish on almost every full level, with the exceptional values independent of any later arc or component.

  1. theorem OAI.CircleDomainRigidity.coarea_L2_errors line 14