OAI/Geometry/PrescribedRicci/JetInterpolation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Jet Interpolation.

  1. def OAI.TameInterpolation.jet line 19
  2. lemma OAI.TameInterpolation.jet_smooth line 24
  3. lemma OAI.TameInterpolation.jet_compact line 31
  4. def OAI.TameInterpolation.jetNorm line 37
  5. lemma OAI.TameInterpolation.lpNorm_jet_le line 40
  6. lemma OAI.TameInterpolation.jetNorm_nonneg line 44
  7. lemma OAI.TameInterpolation.jetNorm_attained line 48
  8. lemma OAI.TameInterpolation.jetNorm_step line 54