OAI/Geometry/Convex/GeneralMahler/TestFun.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Real test functions, all orders of polynomial growth used in the proof.

  1. def OAI.GeneralMahler.Moderate line 9
  2. def OAI.GeneralMahler.TestF line 12
  3. lemma OAI.GeneralMahler.Moderate.poly line 15
  4. lemma OAI.GeneralMahler.Moderate.diff line 16
  5. lemma OAI.GeneralMahler.Moderate.dc line 17
  6. lemma OAI.GeneralMahler.Moderate.der line 21
  7. lemma OAI.GeneralMahler.Moderate.mk line 22
  8. lemma OAI.GeneralMahler.Moderate.mk' line 26
  9. lemma OAI.GeneralMahler.Moderate.mono line 28
  10. lemma OAI.GeneralMahler.Moderate.add line 32
  11. lemma OAI.GeneralMahler.Moderate.neg line 38
  12. lemma OAI.GeneralMahler.Moderate.sub line 43
  13. lemma OAI.GeneralMahler.Moderate.mul line 45
  14. lemma OAI.GeneralMahler.Moderate.ref line 51
  15. lemma OAI.GeneralMahler.Moderate.const line 59
  16. lemma OAI.GeneralMahler.Moderate.id line 63
  17. lemma OAI.GeneralMahler.TestF.of_d line 75
  18. lemma OAI.GeneralMahler.TestF.const line 83
  19. lemma OAI.GeneralMahler.TestF.id line 84
  20. lemma OAI.GeneralMahler.Layers.mc_test line 88
  21. lemma OAI.GeneralMahler.Layers.mj_test line 94
  22. lemma OAI.GeneralMahler.Layers.mw_test line 95
  23. lemma OAI.GeneralMahler.Layers.lc_test line 96
  24. lemma OAI.GeneralMahler.Layers.lp_test line 97