OAI/Geometry/PrescribedRicci/JetTrim.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Jet Trim.

  1. def OAI.TameInterpolation.trimWord line 19
  2. def OAI.TameInterpolation.baseDirection line 23
  3. lemma OAI.TameInterpolation.trimWord_length line 28
  4. lemma OAI.TameInterpolation.trimWord_length_add line 33
  5. def OAI.TameInterpolation.initialJet line 40
  6. lemma OAI.TameInterpolation.initialJet_smooth line 45
  7. lemma OAI.TameInterpolation.initialJet_compact line 52
  8. lemma OAI.TameInterpolation.cword_trim line 59
  9. lemma OAI.TameInterpolation.cword_eq_cjet line 68
  10. lemma OAI.TameInterpolation.trimmed_order line 79
  11. lemma OAI.TameInterpolation.remainder_trimmed_order line 87
  12. theorem OAI.TameInterpolation.monoEval_tame_positive line 97