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

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Interval AD bounding envelopes DD, CQ, KR.

  1. def OAI.GeneralMahler.SCal.Tail.JTB.bmJ line 9
  2. def OAI.GeneralMahler.SCal.Tail.JTB.bnJ line 10
  3. def OAI.GeneralMahler.SCal.Tail.JTB.bt1 line 11
  4. def OAI.GeneralMahler.SCal.Tail.JTB.bPt line 12
  5. def OAI.GeneralMahler.SCal.Tail.JTB.bU line 13
  6. def OAI.GeneralMahler.SCal.Tail.JTB.bPP line 14
  7. def OAI.GeneralMahler.SCal.Tail.JTB.bPQ line 15
  8. def OAI.GeneralMahler.SCal.Tail.JTB.hf0 line 16
  9. def OAI.GeneralMahler.SCal.Tail.JTB.bHH line 17
  10. def OAI.GeneralMahler.SCal.Tail.JTB.bH1 line 18
  11. def OAI.GeneralMahler.SCal.Tail.JTB.bDH line 19
  12. def OAI.GeneralMahler.SCal.Tail.JTB.bM line 20
  13. def OAI.GeneralMahler.SCal.Tail.JTB.bN line 21
  14. def OAI.GeneralMahler.SCal.Tail.JTB.bDel line 22
  15. def OAI.GeneralMahler.SCal.Tail.JTB.bZ line 24
  16. def OAI.GeneralMahler.SCal.Tail.JTB.bA line 25
  17. def OAI.GeneralMahler.SCal.Tail.JTB.bMi line 27
  18. def OAI.GeneralMahler.SCal.Tail.JTB.bN1 line 28
  19. def OAI.GeneralMahler.SCal.Tail.JTB.bDD line 29
  20. def OAI.GeneralMahler.SCal.Tail.JTB.bG line 30
  21. def OAI.GeneralMahler.SCal.Tail.JTB.bKR line 32
  22. def OAI.GeneralMahler.SCal.Tail.JTB.bCQ line 37
  23. def OAI.GeneralMahler.SCal.Tail.JTB.bdF line 39
  24. def OAI.GeneralMahler.SCal.Tail.JTB.bkF line 40
  25. def OAI.GeneralMahler.SCal.Tail.JTB.bcF line 41
  26. lemma OAI.GeneralMahler.SCal.Tail.JTB.mquarter line 43
  27. lemma OAI.GeneralMahler.SCal.Tail.JTB.m32 line 45
  28. lemma OAI.GeneralMahler.SCal.Tail.JTB.fmJ line 50
  29. lemma OAI.GeneralMahler.SCal.Tail.JTB.fnJ line 51
  30. lemma OAI.GeneralMahler.SCal.Tail.JTB.fPt line 52
  31. lemma OAI.GeneralMahler.SCal.Tail.JTB.fU line 53
  32. lemma OAI.GeneralMahler.SCal.Tail.JTB.fPP line 54
  33. lemma OAI.GeneralMahler.SCal.Tail.JTB.fhf0 line 55
  34. lemma OAI.GeneralMahler.SCal.Tail.JTB.fbH line 60
  35. lemma OAI.GeneralMahler.SCal.Tail.JTB.fbH1 line 61
  36. lemma OAI.GeneralMahler.SCal.Tail.JTB.fbDH line 62
  37. lemma OAI.GeneralMahler.SCal.Tail.JTB.fbM line 64
  38. lemma OAI.GeneralMahler.SCal.Tail.JTB.fbN line 65
  39. lemma OAI.GeneralMahler.SCal.Tail.JTB.fbD line 66
  40. lemma OAI.GeneralMahler.SCal.Tail.JTB.fbZ line 69
  41. lemma OAI.GeneralMahler.SCal.Tail.JTB.fbA line 70
  42. lemma OAI.GeneralMahler.SCal.Tail.JTB.fbMi line 72
  43. lemma OAI.GeneralMahler.SCal.Tail.JTB.fDD line 73
  44. lemma OAI.GeneralMahler.SCal.Tail.JTB.fbG line 74
  45. lemma OAI.GeneralMahler.SCal.Tail.JTB.fbN1 line 76
  46. lemma OAI.GeneralMahler.SCal.Tail.JTB.fKR line 77
  47. lemma OAI.GeneralMahler.SCal.Tail.JTB.fCQ line 81
  48. lemma OAI.GeneralMahler.SCal.Tail.JTB.fdF line 83
  49. lemma OAI.GeneralMahler.SCal.Tail.JTB.fcF line 84
  50. lemma OAI.GeneralMahler.SCal.Tail.JTB.fkF line 85