OAI/Analysis/CircleDomains/Sobolev/SmoothSphereCharts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Smooth maps in the concrete sphere charts

This regularity predicate records ordinary real smoothness. For a holomorphic sphere map it follows from complex analyticity in a neighborhood; composition follows from the local chart inverse law.

  1. def OAI.CircleDomainRigidity.IsSmoothSphereAt line 22

    Source documentation

    Real smoothness in the same source and target charts as metric conformality.

    def IsSmoothSphereAt (f : Sphere → Sphere) (p : Sphere) : Prop :=
…

    Mentions: OAI.CircleDomainRigidity.Sphere

  2. def OAI.CircleDomainRigidity.IsSmoothSphereOn line 25
  3. theorem OAI.CircleDomainRigidity.IsSmoothSphereAt.comp line 28
  4. theorem OAI.CircleDomainRigidity.isConformalAt_chartTransform line 47
  5. theorem OAI.CircleDomainRigidity.analyticAt_finite_map_of_conformal line 54
  6. theorem OAI.CircleDomainRigidity.IsConformalOn.isSmoothSphereAt line 74