OAI/Geometry/PrescribedRicci/SmoothLocalInverse.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smooth Local Inverse.

  1. lemma OAI.ExponentialEvaluation.orbit_contDiff line 19
  2. lemma OAI.GlobalElliptic.GluingData.exponentialDensity_contDiff line 41
  3. theorem OAI.GlobalElliptic.GluingData.exists_volume_localInverse line 46
  4. theorem OAI.GlobalElliptic.GluingData.exists_smooth_sobolev_path line 75