OAI/Geometry/PrescribedRicci/CofactorWeakEquation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Cofactor Weak Equation.

  1. lemma OAI.MetricLocalization.cofactor_cutoff_distribution line 21
  2. def OAI.GlobalElliptic.GluingData.outerCompleted line 64
  3. lemma OAI.GlobalElliptic.GluingData.outerCompleted_embed line 68
  4. lemma OAI.GlobalElliptic.GluingData.outerCompleted_embed_add_two line 73
  5. abbrev OAI.GlobalElliptic.GluingData.CofactorPair line 81
  6. def OAI.GlobalElliptic.GluingData.cofactorWeakLeft line 84
  7. def OAI.GlobalElliptic.GluingData.cofactorWeakRight line 92
  8. lemma OAI.GlobalElliptic.GluingData.cofactorWeakLeft_continuous line 101
  9. lemma OAI.GlobalElliptic.GluingData.cofactorCutoff_continuous line 120
  10. lemma OAI.GlobalElliptic.GluingData.cofactorWeakRight_continuous line 144
  11. lemma OAI.GlobalElliptic.GluingData.cofactorWeak_core line 155
  12. lemma OAI.GlobalElliptic.GluingData.cofactor_weak_equation line 178