OAI/Geometry/PrescribedPotential/CalabiResidualBound.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Calabi Residual Bound.

  1. def OAI.KaehlerCalculus.ricciRight line 18
  2. def OAI.KaehlerCalculus.ricciLeft line 21
  3. def OAI.KaehlerCalculus.calabiResidual line 24
  4. lemma OAI.KaehlerCalculus.continuous_ricciRight line 27
  5. lemma OAI.KaehlerCalculus.continuous_ricciLeft line 38
  6. lemma OAI.KaehlerCalculus.ricciRight_smul line 42
  7. lemma OAI.KaehlerCalculus.ricciLeft_smul line 51
  8. lemma OAI.KaehlerCalculus.calabiResidual_homogeneous line 57
  9. lemma OAI.KaehlerCalculus.continuous_calabiResidual line 65
  10. lemma OAI.KaehlerCalculus.tensorSquare_controls_norm line 89
  11. lemma OAI.KaehlerCalculus.calabiResidual_compact_bound line 96