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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

§05 reduction to matrix functionals on linear field.

  1. lemma OAI.GeneralMahler.ProjField.P0_layer line 14
  2. lemma OAI.GeneralMahler.ProjField.H0_layer line 25
  3. lemma OAI.GeneralMahler.ProjField.P_R_bd line 34
  4. def OAI.GeneralMahler.ProjField.scoreE line 52
  5. lemma OAI.GeneralMahler.ProjField.reserve line 54
  6. theorem OAI.GeneralMahler.ProjField.budget line 67