OAI/Analysis/CircleDomains/Sobolev/SphericalBallArea.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quadratic local area growth for the fixed physical sphere metric, at finite points. This compares its actual chart with the area chart.

  1. theorem OAI.CircleDomainRigidity.sphericalArea_singleton line 19
  2. theorem OAI.CircleDomainRigidity.sphericalAreaDensity_le_four line 31
  3. theorem OAI.CircleDomainRigidity.exists_small_spherical_ball_area_bound line 35