OAI/Geometry/PrescribedPotential/CalabiRescue.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Calabi Rescue.

  1. def OAI.KaehlerCalculus.rescueSquare line 19
  2. lemma OAI.KaehlerCalculus.rescueSquare_pos line 22
  3. lemma OAI.KaehlerCalculus.rescueSquare_smul line 39
  4. lemma OAI.KaehlerCalculus.rescueSquare_continuous line 46
  5. lemma OAI.KaehlerCalculus.rescueSquare_compact_lower line 57
  6. def OAI.KaehlerCalculus.LocalKaehlerField.weightedTrace line 80
  7. lemma OAI.KaehlerCalculus.LocalKaehlerField.weightedTrace_smooth line 82
  8. lemma OAI.KaehlerCalculus.LocalKaehlerField.weightedTrace_complex line 91
  9. lemma OAI.KaehlerCalculus.LocalKaehlerField.weightedTrace_laplacian_at_one line 97