OAI/Analysis/CircleDomains/Sobolev/FiniteSphericalArea.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The explicitly defined stereographic spherical area has finite mass. Only integrability, not the exact value of the total area, is needed here.

  1. theorem OAI.CircleDomainRigidity.integrable_sphericalAreaDensity line 19
  2. instance OAI.CircleDomainRigidity.finiteSphericalArea line 28