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

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Towers for q, N profiles and field composition identities.

  1. def OAI.GeneralMahler.SCal.DotF line 9
  2. def OAI.GeneralMahler.SCal.DDot line 10
  3. def OAI.GeneralMahler.SCal.thR line 11
  4. def OAI.GeneralMahler.SCal.NNf line 12
  5. lemma OAI.GeneralMahler.SCal.th_eq line 13
  6. lemma OAI.GeneralMahler.SCal.d_lift line 15
  7. lemma OAI.GeneralMahler.SCal.dd_lift line 18
  8. lemma OAI.GeneralMahler.SCal.SCov line 24
  9. def OAI.GeneralMahler.SCal.CJet.radK line 34
  10. def OAI.GeneralMahler.SCal.CJet.rj line 35
  11. def OAI.GeneralMahler.SCal.CJet.el line 36
  12. def OAI.GeneralMahler.SCal.CJet.qj line 37
  13. def OAI.GeneralMahler.SCal.CJet.it line 38
  14. def OAI.GeneralMahler.SCal.CJet.tj line 39
  15. def OAI.GeneralMahler.SCal.CJet.NJ line 40
  16. def OAI.GeneralMahler.SCal.CJet.Sf line 42
  17. def OAI.GeneralMahler.SCal.CJet.RadH line 46
  18. lemma OAI.GeneralMahler.SCal.CJet.rje line 47
  19. lemma OAI.GeneralMahler.SCal.CJet.qje line 48
  20. lemma OAI.GeneralMahler.SCal.CJet.Ir line 49
  21. lemma OAI.GeneralMahler.SCal.CJet.Ie line 50
  22. lemma OAI.GeneralMahler.SCal.CJet.IQ line 51
  23. lemma OAI.GeneralMahler.SCal.CJet.It line 52
  24. lemma OAI.GeneralMahler.SCal.CJet.IT line 53
  25. lemma OAI.GeneralMahler.SCal.CJet.IN line 54
  26. lemma OAI.GeneralMahler.SCal.CJet.IS line 55
  27. lemma OAI.GeneralMahler.SCal.CJet.nj0 line 58
  28. lemma OAI.GeneralMahler.SCal.CJet.sj0 line 67
  29. def OAI.GeneralMahler.SCal.Row0.bbB line 80
  30. def OAI.GeneralMahler.SCal.Row0.ccB line 81
  31. def OAI.GeneralMahler.SCal.Row0.rB line 82
  32. def OAI.GeneralMahler.SCal.Row0.kkB line 83
  33. def OAI.GeneralMahler.SCal.Row0.radB line 84
  34. def OAI.GeneralMahler.SCal.Row0.Rj line 85
  35. def OAI.GeneralMahler.SCal.Row0.elB line 86
  36. def OAI.GeneralMahler.SCal.Row0.Qj line 87
  37. def OAI.GeneralMahler.SCal.Row0.itB line 88
  38. def OAI.GeneralMahler.SCal.Row0.tjB line 89
  39. def OAI.GeneralMahler.SCal.Row0.NB line 90
  40. def OAI.GeneralMahler.SCal.Row0.SF line 91
  41. lemma OAI.GeneralMahler.SCal.Row0.mbb line 95
  42. lemma OAI.GeneralMahler.SCal.Row0.mcc line 96
  43. lemma OAI.GeneralMahler.SCal.Row0.mrB line 97
  44. lemma OAI.GeneralMahler.SCal.Row0.mradB line 98
  45. lemma OAI.GeneralMahler.SCal.Row0.mkkB line 99
  46. lemma OAI.GeneralMahler.SCal.Row0.At.mRJ line 104
  47. lemma OAI.GeneralMahler.SCal.Row0.At.mQJ line 105
  48. lemma OAI.GeneralMahler.SCal.Row0.At.mit line 106
  49. lemma OAI.GeneralMahler.SCal.Row0.At.mtj line 107
  50. lemma OAI.GeneralMahler.SCal.Row0.At.mNJ line 108
  51. lemma OAI.GeneralMahler.SCal.Row0.At.mSf line 110