OAI/Geometry/Convex/GeneralMahler/Profiles.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

§01 the primary profiles and their identities.

  1. def OAI.GeneralMahler.Profile.X line 11
  2. def OAI.GeneralMahler.Profile.Y line 12
  3. def OAI.GeneralMahler.Profile.f line 13
  4. def OAI.GeneralMahler.Profile.j line 14
  5. def OAI.GeneralMahler.Profile.Xd line 15
  6. def OAI.GeneralMahler.Profile.Yd line 16
  7. def OAI.GeneralMahler.Profile.g line 17
  8. def OAI.GeneralMahler.Profile.d line 18
  9. def OAI.GeneralMahler.Profile.v line 19
  10. def OAI.GeneralMahler.Profile.N line 20
  11. def OAI.GeneralMahler.Profile.N2 line 21
  12. lemma OAI.GeneralMahler.Profile.q_pos line 22
  13. lemma OAI.GeneralMahler.Profile.xp line 23
  14. lemma OAI.GeneralMahler.Profile.yp line 24
  15. lemma OAI.GeneralMahler.Profile.Y_ref line 25
  16. lemma OAI.GeneralMahler.Profile.j_ref line 26
  17. lemma OAI.GeneralMahler.Profile.dX line 27
  18. lemma OAI.GeneralMahler.Profile.dY line 30
  19. def OAI.GeneralMahler.Profile.fd line 34
  20. def OAI.GeneralMahler.Profile.jd line 35
  21. lemma OAI.GeneralMahler.Profile.df line 36
  22. lemma OAI.GeneralMahler.Profile.dj line 39
  23. def OAI.GeneralMahler.Profile.gd line 43
  24. lemma OAI.GeneralMahler.Profile.v_log line 45
  25. lemma OAI.GeneralMahler.Profile.dV line 49
  26. lemma OAI.GeneralMahler.Profile.v_deriv line 53
  27. lemma OAI.GeneralMahler.Profile.C_ids line 55
  28. lemma OAI.GeneralMahler.Profile.dg line 66
  29. lemma OAI.GeneralMahler.Profile.ddX line 72
  30. lemma OAI.GeneralMahler.Profile.ddY line 75
  31. lemma OAI.GeneralMahler.Profile.ddg line 78
  32. lemma OAI.GeneralMahler.Profile.dd line 85
  33. lemma OAI.GeneralMahler.Profile.ddv line 97
  34. lemma OAI.GeneralMahler.Profile.d₃g line 101
  35. lemma OAI.GeneralMahler.Profile.n_identity line 107
  36. lemma OAI.GeneralMahler.Profile.n_d_identity line 108