OAI/Geometry/Convex/GeneralMahler/Budget/Tbound.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

§05 the two layer estimates, retained penalties.

  1. def OAI.GeneralMahler.Profile.ap line 13
  2. def OAI.GeneralMahler.Profile.lm line 14
  3. def OAI.GeneralMahler.Profile.P0 line 15
  4. def OAI.GeneralMahler.Profile.wwR line 16
  5. def OAI.GeneralMahler.Profile.ww line 17
  6. def OAI.GeneralMahler.Profile.ww0 line 18
  7. lemma OAI.GeneralMahler.uy_nn line 21
  8. lemma OAI.GeneralMahler.ux_nn line 31
  9. lemma OAI.GeneralMahler.Bvpp line 41
  10. lemma OAI.GeneralMahler.sq_wt line 42
  11. lemma OAI.GeneralMahler.bhj line 43
  12. lemma OAI.GeneralMahler.P0_wt line 44
  13. lemma OAI.GeneralMahler.Rwt line 47
  14. lemma OAI.GeneralMahler.wwt line 52
  15. lemma OAI.GeneralMahler.w0t line 54
  16. lemma OAI.GeneralMahler.trp line 57
  17. lemma OAI.GeneralMahler.alpha_p line 58
  18. lemma OAI.GeneralMahler.wpos line 60
  19. lemma OAI.GeneralMahler.ProjField.BB_scale line 97
  20. lemma OAI.GeneralMahler.ProjField.BB_add line 104
  21. lemma OAI.GeneralMahler.ProjField.BB_sub line 108
  22. lemma OAI.GeneralMahler.ProjField.BB_bar line 115
  23. lemma OAI.GeneralMahler.ProjField.BB1 line 117
  24. lemma OAI.GeneralMahler.ProjField.block_boxJ line 121
  25. lemma OAI.GeneralMahler.ProjField.limitB line 164