OAI/Geometry/PrescribedRicci/FixedCofactorBootstrap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed Cofactor Bootstrap.

  1. lemma OAI.GlobalElliptic.GluingData.lift_over_lift line 35
  2. lemma OAI.GlobalElliptic.GluingData.cofactor_small_lifted line 44
  3. lemma OAI.GlobalElliptic.GluingData.cofactor_lift_step line 58
  4. lemma OAI.GlobalElliptic.GluingData.cofactor_solution_lifts line 80
  5. lemma OAI.GlobalElliptic.GluingData.realLift_order_witness line 102
  6. lemma OAI.GlobalElliptic.GluingData.cofactor_solution_allRegular line 112
  7. theorem OAI.GlobalElliptic.GluingData.cofactor_solution_smooth line 129