OAI/Geometry/PrescribedRicci/HermitianCoercivity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Hermitian Coercivity.

  1. lemma OAI.MongeAmpere.hermPair_single line 14
  2. lemma OAI.MongeAmpere.hermPair_dual_coordinate line 18
  3. lemma OAI.MongeAmpere.component_sq_le_hermPair line 23
  4. lemma OAI.MongeAmpere.norm_sq_le_hermPair line 29
  5. lemma OAI.MongeAmpere.pair_norm_le line 45