OAI/Geometry/PrescribedRicci/TameCofactorGain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Tame Cofactor Gain.

  1. lemma OAI.GlobalElliptic.GluingData.cofactor_local_gain line 32
  2. lemma OAI.GlobalElliptic.GluingData.real_sobolev_of_local_order line 76
  3. lemma OAI.GlobalElliptic.GluingData.real_sobolev_of_local_order_eq line 93
  4. theorem OAI.GlobalElliptic.GluingData.cofactor_global_gain line 104