OAI/Geometry/PrescribedRicci/CalabiTensorBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Calabi Tensor Bounds.

  1. lemma OAI.MongeAmpere.tensor3_norm_le line 17
  2. lemma OAI.MongeAmpere.tensorMetric_inv line 28
  3. lemma OAI.MongeAmpere.tensorMetric_norm_bound line 35
  4. lemma OAI.MongeAmpere.tensorMetric_inv_norm_bound line 44
  5. lemma OAI.MongeAmpere.tensorConnection_norm_le line 54
  6. lemma OAI.MongeAmpere.matrix_norm_mul_le line 81
  7. lemma OAI.MongeAmpere.mulVec_norm_le line 88