OAI/Analysis/CircleDomains/Sobolev/SphereChartLipschitz.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The fixed physical sphere metric has locally Lipschitz finite charts. This follows from the explicit smooth inverse stereographic formula in Mathlib, including the linear coordinates chosen by the sphere homeomorphism.

  1. abbrev OAI.CircleDomainRigidity.RoundAmbient line 17
  2. theorem OAI.CircleDomainRigidity.contDiff_roundSphere_finite_chart line 19
  3. theorem OAI.CircleDomainRigidity.finite_sphere_chart_locally_lipschitz line 34
  4. theorem OAI.CircleDomainRigidity.finite_sphere_chart_lipschitz_on_compact line 43