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

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

§07 stable algebra shared by finite and infinite estimates.

  1. def OAI.GeneralMahler.SCal.sY line 12
  2. def OAI.GeneralMahler.SCal.sB line 13
  3. def OAI.GeneralMahler.SCal.sU line 14
  4. def OAI.GeneralMahler.SCal.sP line 15
  5. def OAI.GeneralMahler.SCal.sJ line 16
  6. def OAI.GeneralMahler.SCal.sH line 17
  7. def OAI.GeneralMahler.SCal.sW line 18
  8. def OAI.GeneralMahler.SCal.sd line 19
  9. def OAI.GeneralMahler.SCal.sK line 20
  10. def OAI.GeneralMahler.SCal.sg1 line 21
  11. def OAI.GeneralMahler.SCal.sC line 22
  12. def OAI.GeneralMahler.SCal.sRv line 23
  13. def OAI.GeneralMahler.SCal.sV2 line 24
  14. lemma OAI.GeneralMahler.SCal.u_eq' line 25
  15. lemma OAI.GeneralMahler.SCal.u_pos line 27
  16. lemma OAI.GeneralMahler.SCal.u_le line 28
  17. lemma OAI.GeneralMahler.SCal.sPe line 29
  18. lemma OAI.GeneralMahler.SCal.h_f line 30
  19. lemma OAI.GeneralMahler.SCal.lp_st line 33
  20. lemma OAI.GeneralMahler.SCal.B_st line 38
  21. lemma OAI.GeneralMahler.SCal.Xu line 39
  22. lemma OAI.GeneralMahler.SCal.X1u line 41
  23. lemma OAI.GeneralMahler.SCal.YDst line 44
  24. lemma OAI.GeneralMahler.SCal.d_stable line 45
  25. lemma OAI.GeneralMahler.SCal.k_stable line 47
  26. lemma OAI.GeneralMahler.SCal.g_stable line 52
  27. lemma OAI.GeneralMahler.SCal.c_stable line 57
  28. lemma OAI.GeneralMahler.SCal.sY_ident line 59
  29. lemma OAI.GeneralMahler.SCal.sJneg line 62
  30. lemma OAI.GeneralMahler.SCal.rv_stable line 66
  31. lemma OAI.GeneralMahler.SCal.v2_stable line 68
  32. def OAI.GeneralMahler.SCal.xs line 74
  33. def OAI.GeneralMahler.SCal.ast line 75
  34. def OAI.GeneralMahler.SCal.liftF line 76
  35. lemma OAI.GeneralMahler.SCal.hsb line 77
  36. lemma OAI.GeneralMahler.SCal.xD line 78
  37. lemma OAI.GeneralMahler.SCal.aD line 79
  38. lemma OAI.GeneralMahler.SCal.ap line 80
  39. lemma OAI.GeneralMahler.SCal.x_mono line 81
  40. lemma OAI.GeneralMahler.SCal.x_ang line 82
  41. lemma OAI.GeneralMahler.SCal.ontoX line 84