OAI/Geometry/Convex/GeneralMahler/Scalar/Tail/Coords.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Convert tail jets into coordinate and number operator bounds.

  1. def OAI.GeneralMahler.SCal.Tail.rrF line 9
  2. def OAI.GeneralMahler.SCal.Tail.ql line 10
  3. lemma OAI.GeneralMahler.SCal.Tail.rre0 line 13
  4. lemma OAI.GeneralMahler.SCal.Tail.qe0 line 14
  5. lemma OAI.GeneralMahler.SCal.Tail.Twq line 15
  6. def OAI.GeneralMahler.SCal.Tail.bt line 18
  7. lemma OAI.GeneralMahler.SCal.Tail.dots_log line 19
  8. lemma OAI.GeneralMahler.SCal.Tail.bt_bound line 38
  9. def OAI.GeneralMahler.SCal.Tail.bRat line 53
  10. def OAI.GeneralMahler.SCal.Tail.bRj line 54
  11. def OAI.GeneralMahler.SCal.Tail.bQj line 55
  12. def OAI.GeneralMahler.SCal.Tail.ba line 57
  13. def OAI.GeneralMahler.SCal.Tail.bbN line 58
  14. def OAI.GeneralMahler.SCal.Tail.bdN line 59
  15. def OAI.GeneralMahler.SCal.Tail.bS2 line 60
  16. lemma OAI.GeneralMahler.SCal.Tail.mRj line 62
  17. lemma OAI.GeneralMahler.SCal.Tail.mqReduce line 64
  18. lemma OAI.GeneralMahler.SCal.Tail.mQl line 68
  19. lemma OAI.GeneralMahler.SCal.Tail.mDots line 69