OAI/Analysis/CircleDomains/Sobolev/ExteriorAngularEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact angular-energy lower bound in the nonnegative integral used by polar change of variables.

  1. lemma OAI.CircleDomainRigidity.exterior_derivative_angular_energy line 13