OAI/Geometry/Convex/GeneralMahler/Scalar/BoxJ.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Interval enclosures for profile derivative towers from hyperbolic coordinates and bounds for the Laplace moments Ymk.

  1. structure OAI.GeneralMahler.SCal.Row0 line 11
  2. def OAI.GeneralMahler.SCal.Row0.sbB line 17
  3. def OAI.GeneralMahler.SCal.Row0.arB line 18
  4. def OAI.GeneralMahler.SCal.Row0.bSinh line 19
  5. def OAI.GeneralMahler.SCal.Row0.bCosh line 20
  6. lemma OAI.GeneralMahler.SCal.Row0.msbB line 21
  7. lemma OAI.GeneralMahler.SCal.Row0.marB line 24
  8. lemma OAI.GeneralMahler.SCal.Row0.mHyp line 27
  9. def OAI.GeneralMahler.SCal.Row0.point line 31
  10. def OAI.GeneralMahler.SCal.Row0.around line 35
  11. structure OAI.GeneralMahler.SCal.Row0.At line 38
  12. lemma OAI.GeneralMahler.SCal.Row0.at_point line 42
  13. lemma OAI.GeneralMahler.SCal.Row0.at_segment line 46
  14. def OAI.GeneralMahler.SCal.Row0.Xj line 61
  15. def OAI.GeneralMahler.SCal.Row0.Ym line 62
  16. def OAI.GeneralMahler.SCal.Row0.Y line 63
  17. def OAI.GeneralMahler.SCal.Row0.B line 64
  18. def OAI.GeneralMahler.SCal.Row0.hsS line 65
  19. def OAI.GeneralMahler.SCal.Row0.Ph line 66
  20. def OAI.GeneralMahler.SCal.Row0.U line 69
  21. def OAI.GeneralMahler.SCal.Row0.P0 line 70
  22. def OAI.GeneralMahler.SCal.Row0.W0 line 71
  23. def OAI.GeneralMahler.SCal.Row0.Hj line 72
  24. def OAI.GeneralMahler.SCal.Row0.J0 line 75
  25. def OAI.GeneralMahler.SCal.Row0.Dj line 79
  26. def OAI.GeneralMahler.SCal.Row0.Kj line 80
  27. def OAI.GeneralMahler.SCal.Row0.Gp line 82
  28. def OAI.GeneralMahler.SCal.Row0.Cj line 83
  29. def OAI.GeneralMahler.SCal.Row0.Mc line 84
  30. def OAI.GeneralMahler.SCal.Row0.JY line 85
  31. def OAI.GeneralMahler.SCal.Row0.Rv line 86
  32. def OAI.GeneralMahler.SCal.Row0.Vv line 87
  33. lemma OAI.GeneralMahler.SCal.Row0.At.mXj line 93
  34. lemma OAI.GeneralMahler.SCal.Row0.At.ms line 99
  35. lemma OAI.GeneralMahler.SCal.Row0.At.mP line 101
  36. lemma OAI.GeneralMahler.SCal.Row0.At.mY line 104
  37. lemma OAI.GeneralMahler.SCal.Row0.At.mU line 109
  38. lemma OAI.GeneralMahler.SCal.Row0.At.mP0 line 110
  39. lemma OAI.GeneralMahler.SCal.Row0.At.mW line 111
  40. lemma OAI.GeneralMahler.SCal.Row0.At.mH line 112
  41. lemma OAI.GeneralMahler.SCal.Row0.At.mJ line 121
  42. lemma OAI.GeneralMahler.SCal.Row0.At.mD line 124
  43. lemma OAI.GeneralMahler.SCal.Row0.At.mK line 126
  44. lemma OAI.GeneralMahler.SCal.Row0.At.mC line 128
  45. lemma OAI.GeneralMahler.SCal.Row0.At.mMc line 131
  46. lemma OAI.GeneralMahler.SCal.Row0.At.mJy line 132
  47. lemma OAI.GeneralMahler.SCal.Row0.At.mRv line 133
  48. lemma OAI.GeneralMahler.SCal.Row0.At.mVv line 134