OAI/Analysis/CircleDomains/Sobolev/SobolevCoareaProof.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact weighted Sobolev coarea input is proved from the closed Lipschitz representatives, their actual gradients, and the null-fiber result for the remaining volume-null set.

  1. lemma OAI.CircleDomainRigidity.physical_field_coarea_null line 16
  2. lemma OAI.CircleDomainRigidity.planarSobolevCoarea line 30