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

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

§07 tail profile identities using normalized log towers.

  1. def OAI.GeneralMahler.SCal.Tail.JT.MJ line 12
  2. def OAI.GeneralMahler.SCal.Tail.JT.NJ line 13
  3. def OAI.GeneralMahler.SCal.Tail.JT.Pt line 14
  4. def OAI.GeneralMahler.SCal.Tail.JT.U line 15
  5. def OAI.GeneralMahler.SCal.Tail.JT.PP line 16
  6. def OAI.GeneralMahler.SCal.Tail.JT.PQ line 17
  7. def OAI.GeneralMahler.SCal.Tail.JT.HH line 18
  8. def OAI.GeneralMahler.SCal.Tail.JT.H1 line 19
  9. def OAI.GeneralMahler.SCal.Tail.JT.DH line 20
  10. def OAI.GeneralMahler.SCal.Tail.JT.M2 line 21
  11. def OAI.GeneralMahler.SCal.Tail.JT.NN line 22
  12. def OAI.GeneralMahler.SCal.Tail.JT.del line 23
  13. def OAI.GeneralMahler.SCal.Tail.JT.wZ line 25
  14. def OAI.GeneralMahler.SCal.Tail.JT.A line 26
  15. def OAI.GeneralMahler.SCal.Tail.JT.mi line 28
  16. def OAI.GeneralMahler.SCal.Tail.JT.N1 line 29
  17. def OAI.GeneralMahler.SCal.Tail.JT.DD line 30
  18. def OAI.GeneralMahler.SCal.Tail.JT.G0 line 31
  19. def OAI.GeneralMahler.SCal.Tail.JT.KR line 33
  20. def OAI.GeneralMahler.SCal.Tail.JT.CQ line 38
  21. def OAI.GeneralMahler.SCal.Tail.JT.dF line 39
  22. def OAI.GeneralMahler.SCal.Tail.JT.kF line 40
  23. def OAI.GeneralMahler.SCal.Tail.JT.gF line 41
  24. def OAI.GeneralMahler.SCal.Tail.JT.cF line 42
  25. lemma OAI.GeneralMahler.SCal.Tail.JT.ym_id line 44
  26. lemma OAI.GeneralMahler.SCal.Tail.JT.n_id line 45
  27. lemma OAI.GeneralMahler.SCal.Tail.JT.pt0 line 47
  28. lemma OAI.GeneralMahler.SCal.Tail.JT.U0 line 50
  29. lemma OAI.GeneralMahler.SCal.Tail.JT.MPv line 54
  30. lemma OAI.GeneralMahler.SCal.Tail.JT.Nv line 55
  31. lemma OAI.GeneralMahler.SCal.Tail.JT.mi_id line 56
  32. lemma OAI.GeneralMahler.SCal.Tail.JT.P0 line 59
  33. lemma OAI.GeneralMahler.SCal.Tail.JT.H0 line 60
  34. lemma OAI.GeneralMahler.SCal.Tail.JT.ht1 line 64
  35. lemma OAI.GeneralMahler.SCal.Tail.JT.DH0 line 81
  36. lemma OAI.GeneralMahler.SCal.Tail.JT.WZ0 line 92
  37. lemma OAI.GeneralMahler.SCal.Tail.JT.dF0 line 101
  38. lemma OAI.GeneralMahler.SCal.Tail.JT.gF0 line 110
  39. lemma OAI.GeneralMahler.SCal.Tail.JT.kF0 line 120
  40. lemma OAI.GeneralMahler.SCal.Tail.JT.TeM line 133
  41. lemma OAI.GeneralMahler.SCal.Tail.JT.TeN line 134
  42. lemma OAI.GeneralMahler.SCal.Tail.JT.TeP line 135
  43. lemma OAI.GeneralMahler.SCal.Tail.JT.TeU line 136
  44. lemma OAI.GeneralMahler.SCal.Tail.JT.TePP line 137
  45. lemma OAI.GeneralMahler.SCal.Tail.JT.huJ line 138
  46. lemma OAI.GeneralMahler.SCal.Tail.JT.ppj line 139
  47. lemma OAI.GeneralMahler.SCal.Tail.JT.TeH line 140
  48. lemma OAI.GeneralMahler.SCal.Tail.JT.TeH1 line 141
  49. lemma OAI.GeneralMahler.SCal.Tail.JT.Ted line 142
  50. lemma OAI.GeneralMahler.SCal.Tail.JT.TeZ line 145
  51. lemma OAI.GeneralMahler.SCal.Tail.JT.Tem2 line 146
  52. lemma OAI.GeneralMahler.SCal.Tail.JT.Ten2 line 147
  53. lemma OAI.GeneralMahler.SCal.Tail.JT.Temi line 148
  54. lemma OAI.GeneralMahler.SCal.Tail.JT.TeG line 149
  55. lemma OAI.GeneralMahler.SCal.Tail.JT.TeA line 151
  56. lemma OAI.GeneralMahler.SCal.Tail.JT.TeDH line 152
  57. lemma OAI.GeneralMahler.SCal.Tail.JT.TeDD line 154
  58. lemma OAI.GeneralMahler.SCal.Tail.JT.TeN1 line 155
  59. lemma OAI.GeneralMahler.SCal.Tail.JT.TeKR line 156
  60. lemma OAI.GeneralMahler.SCal.Tail.JT.TeCQ line 159
  61. lemma OAI.GeneralMahler.SCal.Tail.JT.TdF line 160
  62. lemma OAI.GeneralMahler.SCal.Tail.JT.TkF line 161
  63. lemma OAI.GeneralMahler.SCal.Tail.JT.TgF line 162
  64. lemma OAI.GeneralMahler.SCal.Tail.JT.TcF line 163
  65. lemma OAI.GeneralMahler.SCal.Tail.JT.path line 165
  66. lemma OAI.GeneralMahler.SCal.Tail.JT.cF0 line 181