OAI/Geometry/PrescribedPotential/CalabiCoordinateBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Calabi Coordinate Bound.

  1. lemma OAI.KaehlerCalculus.matrix_mul_elementwise_bound line 19
  2. lemma OAI.KaehlerCalculus.hol_matrix_stencil_bound line 34
  3. lemma OAI.KaehlerCalculus.LocalKaehlerField.holDerivative_connection line 47
  4. lemma OAI.KaehlerCalculus.LocalKaehlerField.fderiv_eq_hol_add_star line 52
  5. lemma OAI.KaehlerCalculus.LocalKaehlerField.matrix_fderiv_bound line 71
  6. theorem OAI.KaehlerCalculus.calabi_coordinate_connection_uniform line 99
  7. theorem OAI.KaehlerCalculus.calabi_coordinate_C1_uniform line 139