OAI/MathematicalPhysics/AlternatingFlow/CertifiedBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Effective.weight line 14
  2. lemma OAI.AlternatingNS.Effective.weight_pos line 16
  3. def OAI.AlternatingNS.Effective.Certified line 18
  4. lemma OAI.AlternatingNS.Effective.velocity_certified line 22
  5. lemma OAI.AlternatingNS.Effective.Certified.congr line 72
  6. lemma OAI.AlternatingNS.Effective.Certified.param line 75
  7. lemma OAI.AlternatingNS.Effective.Certified.add line 80
  8. lemma OAI.AlternatingNS.Effective.Certified.linear line 93
  9. lemma OAI.AlternatingNS.Effective.Certified.csmul line 105
  10. lemma OAI.AlternatingNS.Effective.Certified.sub line 112
  11. lemma OAI.AlternatingNS.Effective.Certified.directional line 116
  12. lemma OAI.AlternatingNS.Effective.Certified.smul line 128