OAI/Analysis/CircleDomains/Sobolev/CoareaL2Weight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A locally square-integrable weight is integrable on almost every bounded scalar Sobolev level.

  1. theorem OAI.CircleDomainRigidity.coarea_L2_weight_finite line 12