OAI/Geometry/PrescribedRicci/FiniteCofactor.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite Cofactor.

  1. lemma OAI.GlobalElliptic.Localizers.strong_lower line 27
  2. lemma OAI.GlobalElliptic.GluingData.completedHessian_lower line 40
  3. lemma OAI.GlobalElliptic.GluingData.completedRealify_strong line 53
  4. def OAI.GlobalElliptic.GluingData.cofactorMatrix line 65
  5. def OAI.GlobalElliptic.GluingData.cofactorScalar line 68
  6. lemma OAI.GlobalElliptic.GluingData.cofactorScalar_continuous line 75
  7. lemma OAI.GlobalElliptic.GluingData.cofactorScalar_strong line 83
  8. lemma OAI.GlobalElliptic.GluingData.cofactorScalar_zero_source line 98
  9. lemma OAI.GlobalElliptic.GluingData.cofactorScalar_strong_lower line 115