OAI/Geometry/PrescribedPotential/CalabiCoordinateCoercivity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Calabi Coordinate Coercivity.

  1. def OAI.KaehlerCalculus.tensorTransport line 20
  2. lemma OAI.KaehlerCalculus.tensorTransport_smul line 23
  3. lemma OAI.KaehlerCalculus.tensorTransport_zero line 29
  4. lemma OAI.KaehlerCalculus.tensorTransport_undo line 34
  5. lemma OAI.KaehlerCalculus.continuous_tensorTransport line 63
  6. lemma OAI.KaehlerCalculus.boundedFrame_tensor_coercivity line 76
  7. lemma OAI.KaehlerCalculus.connection_norm_bound_of_frame line 90