OAI/Analysis/CircleDomains/Sobolev/RegularPieceCoarea.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Coarea on a bounded regular measurable set, using its actual scalar coordinate map and the countable bi-Lipschitz decomposition.

  1. lemma OAI.CircleDomainRigidity.weighted_coarea_empty line 14
  2. lemma OAI.CircleDomainRigidity.regular_piece_weighted_coarea line 24
  3. lemma OAI.CircleDomainRigidity.regular_map_weighted_coarea line 51