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

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Constant-layer penalty and commutator remainder accounting.

  1. def OAI.GeneralMahler.ProjField.NK line 13
  2. lemma OAI.GeneralMahler.ProjField.nn_eq line 14
  3. lemma OAI.GeneralMahler.ProjField.NKpos line 17
  4. lemma OAI.GeneralMahler.ProjField.lm_pos line 22
  5. lemma OAI.GeneralMahler.ProjField.karp line 23
  6. lemma OAI.GeneralMahler.ProjField.LL1 line 25
  7. lemma OAI.GeneralMahler.ProjField.NZ_A line 28
  8. lemma OAI.GeneralMahler.ProjField.NZ_L line 44
  9. lemma OAI.GeneralMahler.ProjField.const_limit line 51
  10. lemma OAI.GeneralMahler.ProjField.cmCL line 92
  11. lemma OAI.GeneralMahler.ProjField.C_Hcomm line 95
  12. lemma OAI.GeneralMahler.ProjField.comm_split line 109
  13. lemma OAI.GeneralMahler.ProjField.comm_est line 131
  14. lemma OAI.GeneralMahler.ProjField.comm_bound line 157