OAI/Analysis/CircleDomains/Sobolev/SphericalAreaLocalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Local planar square integrability from spherical area. Spherical area is written in its finite stereographic chart, with density 4/(1+|z|²)².

  1. def OAI.CircleDomainRigidity.sphericalAreaDensity line 20
  2. theorem OAI.CircleDomainRigidity.sphericalAreaDensity_pos line 22
  3. theorem OAI.CircleDomainRigidity.continuous_sphericalAreaDensity line 26
  4. def OAI.CircleDomainRigidity.sphericalArea line 31
  5. theorem OAI.CircleDomainRigidity.lintegral_sphericalArea line 35
  6. theorem OAI.CircleDomainRigidity.planar_energy_on_compact_finite line 43
  7. theorem OAI.CircleDomainRigidity.planar_energy_quotient_neighborhood_finite line 69