OAI/Geometry/PrescribedRicci/MatrixCompactBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Matrix Compact Bounds.

  1. lemma OAI.MongeAmpere.compact_matrix_bound line 14
  2. lemma OAI.MongeAmpere.matrix_norm_le_of_entries line 21
  3. lemma OAI.MongeAmpere.posDef_eq_det_smul_adjugate_inv line 29
  4. lemma OAI.MongeAmpere.posDef_norm_det line 37
  5. lemma OAI.MongeAmpere.metric_norm_bound_from_inverse line 42