OAI/Geometry/Convex/GeneralMahler/Linear/Nu.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Positive endpoint functional Nu.

  1. def OAI.GeneralMahler.LPt.npt line 13
  2. def OAI.GeneralMahler.LPt.mout line 15
  3. lemma OAI.GeneralMahler.LPt.n_add line 18
  4. lemma OAI.GeneralMahler.LPt.n_sub line 21
  5. lemma OAI.GeneralMahler.LPt.n_s line 25
  6. lemma OAI.GeneralMahler.LPt.n_flip line 29
  7. lemma OAI.GeneralMahler.LPt.hsout line 35
  8. lemma OAI.GeneralMahler.LPt.ipnout line 40
  9. lemma OAI.GeneralMahler.LPt.out_her line 45
  10. def OAI.GeneralMahler.ProjField.nupt line 56
  11. def OAI.GeneralMahler.ProjField.nu line 58
  12. lemma OAI.GeneralMahler.ProjField.ContLoc line 63
  13. lemma OAI.GeneralMahler.ProjField.MeasLoc line 68
  14. lemma OAI.GeneralMahler.ProjField.locMe line 70
  15. lemma OAI.GeneralMahler.ProjField.nu_i line 78
  16. lemma OAI.GeneralMahler.ProjField.nu_add line 92
  17. lemma OAI.GeneralMahler.ProjField.nu_sub line 97
  18. lemma OAI.GeneralMahler.ProjField.nu_s line 101
  19. lemma OAI.GeneralMahler.ProjField.nu_flip line 104