OAI/MathematicalPhysics/AlternatingFlow/RecursiveBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AlternatingNS.Effective.nat_sum_range line 13
  2. def OAI.AlternatingNS.Effective.Scaled line 27
  3. lemma OAI.AlternatingNS.Effective.Scaled.congr line 37
  4. lemma OAI.AlternatingNS.Effective.Scaled.param line 41
  5. lemma OAI.AlternatingNS.Effective.Scaled.const line 47
  6. lemma OAI.AlternatingNS.Effective.Scaled.add line 58
  7. lemma OAI.AlternatingNS.Effective.Scaled.sub line 69
  8. lemma OAI.AlternatingNS.Effective.Scaled.smul line 80
  9. lemma OAI.AlternatingNS.Effective.Scaled.mul line 93
  10. lemma OAI.AlternatingNS.Effective.Scaled.ite line 128
  11. lemma OAI.AlternatingNS.Effective.Scaled.sum_range line 140
  12. lemma OAI.AlternatingNS.Effective.Scaled.comp line 155
  13. lemma OAI.AlternatingNS.Effective.Scaled.comp_linear line 191
  14. lemma OAI.AlternatingNS.Effective.Scaled.comp_scaled_linear line 208
  15. lemma OAI.AlternatingNS.Effective.Scaled.fixed line 218