OAI/Analysis/CircleDomains/Sobolev/SobolevGraphEnergyRegular.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual Sobolev graph energy is locally finite and outer regular. A volume-null base set has zero graph energy.

  1. lemma OAI.CircleDomainRigidity.sobolevGraph_injective line 14
  2. lemma OAI.CircleDomainRigidity.sobolevGraphEnergy_finiteOnCompacts line 18
  3. lemma OAI.CircleDomainRigidity.sobolevGraphEnergy_outerRegular line 45
  4. lemma OAI.CircleDomainRigidity.sobolevGraphEnergy_null line 52