OAI/Geometry/PrescribedRicci/ComplexJet.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Complex Jet.

  1. def OAI.TameInterpolation.cdir line 20
  2. lemma OAI.TameInterpolation.cdir_smooth line 23
  3. lemma OAI.TameInterpolation.cdir_compact line 27
  4. def OAI.TameInterpolation.cjet line 31
  5. lemma OAI.TameInterpolation.cjet_smooth line 37
  6. lemma OAI.TameInterpolation.cjet_compact line 45
  7. lemma OAI.TameInterpolation.cjet_real_map line 53
  8. def OAI.TameInterpolation.realComponents line 65
  9. lemma OAI.TameInterpolation.realComponents_smooth line 70
  10. lemma OAI.TameInterpolation.realComponents_compact line 78
  11. lemma OAI.TameInterpolation.lpNorm_complex_le line 84
  12. lemma OAI.TameInterpolation.cjet_lpNorm_le line 92