OAI/Geometry/PrescribedRicci/LocalizedPathData.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Localized Path Data.

  1. def OAI.GlobalElliptic.cutMetric line 20
  2. lemma OAI.GlobalElliptic.cutMetric_apply line 26
  3. lemma OAI.GlobalElliptic.localize_cutoff_germ line 30
  4. lemma OAI.GlobalElliptic.localized_hessian_germ line 39
  5. lemma OAI.GlobalElliptic.cutMetric_deform line 58
  6. lemma OAI.GlobalElliptic.cutMetric_deform_germ line 76
  7. lemma OAI.GlobalElliptic.schwartzWord_real line 89
  8. lemma OAI.GlobalElliptic.localize_cutoff_real line 108