OAI/MathematicalPhysics/AlternatingFlow/JetNames.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Effective.direction line 12
  2. lemma OAI.AlternatingNS.Effective.direction_norm line 15
  3. def OAI.AlternatingNS.Effective.shift line 18
  4. lemma OAI.AlternatingNS.Effective.shift_computable line 24
  5. lemma OAI.AlternatingNS.Effective.shift_cast line 38
  6. def OAI.AlternatingNS.Effective.wordJet line 43
  7. lemma OAI.AlternatingNS.Effective.wordJet_smooth line 48
  8. lemma OAI.AlternatingNS.Effective.wordJet_bound line 55
  9. lemma OAI.AlternatingNS.Effective.jet_lipschitz line 67
  10. lemma OAI.AlternatingNS.Effective.difference_error line 76
  11. lemma OAI.AlternatingNS.Effective.tolerance_add line 98
  12. lemma OAI.AlternatingNS.Effective.nat_mul_tolerance line 101
  13. lemma OAI.AlternatingNS.Effective.difference_precision line 107