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

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Finite-real-variable towers in t coordinate.

  1. def OAI.GeneralMahler.SCal.xj line 11
  2. def OAI.GeneralMahler.SCal.aj line 12
  3. lemma OAI.GeneralMahler.SCal.xj0 line 13
  4. lemma OAI.GeneralMahler.SCal.aj0 line 14
  5. lemma OAI.GeneralMahler.SCal.Ix line 15
  6. lemma OAI.GeneralMahler.SCal.Ia line 22
  7. def OAI.GeneralMahler.SCal.momRF line 24
  8. def OAI.GeneralMahler.SCal.hfRF line 25
  9. lemma OAI.GeneralMahler.SCal.Imom line 26
  10. lemma OAI.GeneralMahler.SCal.Ihf line 30
  11. def OAI.GeneralMahler.SCal.CJet.halfS line 36
  12. def OAI.GeneralMahler.SCal.CJet.etaS line 37
  13. def OAI.GeneralMahler.SCal.CJet.ph line 38
  14. def OAI.GeneralMahler.SCal.CJet.ym line 39
  15. def OAI.GeneralMahler.SCal.CJet.Y line 40
  16. def OAI.GeneralMahler.SCal.CJet.B line 41
  17. def OAI.GeneralMahler.SCal.CJet.u line 42
  18. def OAI.GeneralMahler.SCal.CJet.p0 line 43
  19. def OAI.GeneralMahler.SCal.CJet.h line 44
  20. def OAI.GeneralMahler.SCal.CJet.j line 45
  21. def OAI.GeneralMahler.SCal.CJet.w line 48
  22. def OAI.GeneralMahler.SCal.CJet.dj line 49
  23. def OAI.GeneralMahler.SCal.CJet.gp line 50
  24. def OAI.GeneralMahler.SCal.CJet.kj line 51
  25. def OAI.GeneralMahler.SCal.CJet.cj line 53
  26. def OAI.GeneralMahler.SCal.CJet.mc line 54
  27. def OAI.GeneralMahler.SCal.CJet.jy line 55
  28. def OAI.GeneralMahler.SCal.CJet.rv line 56
  29. def OAI.GeneralMahler.SCal.CJet.vv line 57
  30. lemma OAI.GeneralMahler.SCal.CJet.hs0 line 60
  31. lemma OAI.GeneralMahler.SCal.CJet.ph0 line 62
  32. lemma OAI.GeneralMahler.SCal.CJet.ym0 line 65
  33. lemma OAI.GeneralMahler.SCal.CJet.Y0 line 68
  34. lemma OAI.GeneralMahler.SCal.CJet.B0 line 69
  35. lemma OAI.GeneralMahler.SCal.CJet.u0 line 70
  36. lemma OAI.GeneralMahler.SCal.CJet.p0v line 72
  37. lemma OAI.GeneralMahler.SCal.CJet.h0 line 73
  38. lemma OAI.GeneralMahler.SCal.CJet.j0 line 76
  39. lemma OAI.GeneralMahler.SCal.CJet.wst line 79
  40. lemma OAI.GeneralMahler.SCal.CJet.d0s line 80
  41. lemma OAI.GeneralMahler.SCal.CJet.k0s line 83
  42. lemma OAI.GeneralMahler.SCal.CJet.c0s line 86
  43. lemma OAI.GeneralMahler.SCal.CJet.krv line 89
  44. lemma OAI.GeneralMahler.SCal.CJet.kvv line 92
  45. lemma OAI.GeneralMahler.SCal.CJet.Ih line 96
  46. lemma OAI.GeneralMahler.SCal.CJet.Iph line 97
  47. lemma OAI.GeneralMahler.SCal.CJet.IY line 98
  48. lemma OAI.GeneralMahler.SCal.CJet.Iu line 99
  49. lemma OAI.GeneralMahler.SCal.CJet.Ip line 100
  50. lemma OAI.GeneralMahler.SCal.CJet.ypJ line 101
  51. lemma OAI.GeneralMahler.SCal.CJet.ppJ line 102
  52. lemma OAI.GeneralMahler.SCal.CJet.IhJ line 103
  53. lemma OAI.GeneralMahler.SCal.CJet.Ij line 104
  54. lemma OAI.GeneralMahler.SCal.CJet.Iw line 105
  55. lemma OAI.GeneralMahler.SCal.CJet.Id line 106
  56. lemma OAI.GeneralMahler.SCal.CJet.Ig line 107
  57. lemma OAI.GeneralMahler.SCal.CJet.IK line 108
  58. lemma OAI.GeneralMahler.SCal.CJet.IC line 109
  59. lemma OAI.GeneralMahler.SCal.CJet.Ijy line 110
  60. lemma OAI.GeneralMahler.SCal.CJet.Imc line 111
  61. lemma OAI.GeneralMahler.SCal.CJet.Irv line 112
  62. lemma OAI.GeneralMahler.SCal.CJet.Ivv line 113