OAI/Geometry/PrescribedRicci/CofactorLocalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Cofactor Localization.

  1. def OAI.GlobalElliptic.GluingData.outerCore line 24
  2. def OAI.GlobalElliptic.GluingData.weightCore line 28
  3. lemma OAI.GlobalElliptic.GluingData.outerCore_eventually line 30
  4. lemma OAI.GlobalElliptic.GluingData.outerHessian_source line 38
  5. lemma OAI.GlobalElliptic.GluingData.cofactorDifferential_source line 49
  6. lemma OAI.GlobalElliptic.GluingData.weightCore_apply line 79
  7. lemma OAI.GlobalElliptic.GluingData.weightCore_outerCore line 88