OAI/Geometry/Convex/GeneralMahler/Forms.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Forms on the Hermite coefficients. D and sigma in paper §04.

  1. lemma OAI.GeneralMahler.pj_ss line 13
  2. lemma OAI.GeneralMahler.pJ_smul_left line 17
  3. lemma OAI.GeneralMahler.pJ_smul_right line 19
  4. lemma OAI.GeneralMahler.pj_poly_part line 22
  5. def OAI.GeneralMahler.ProjField.DLMat line 29
  6. def OAI.GeneralMahler.ProjField.dirF line 30
  7. lemma OAI.GeneralMahler.ProjField.dl_raise line 32
  8. lemma OAI.GeneralMahler.ProjField.Pt_dir line 42
  9. def OAI.GeneralMahler.ProjField.DD line 67
  10. def OAI.GeneralMahler.ProjField.Dterm line 68
  11. def OAI.GeneralMahler.ProjField.Dnorm line 69
  12. def OAI.GeneralMahler.ProjField.RR line 71
  13. def OAI.GeneralMahler.ProjField.sigterm line 72
  14. def OAI.GeneralMahler.ProjField.sigma line 73
  15. lemma OAI.GeneralMahler.ProjField.H_K_split line 75
  16. lemma OAI.GeneralMahler.ProjField.R_reg line 99
  17. lemma OAI.GeneralMahler.ProjField.sig_split line 101
  18. def OAI.GeneralMahler.ProjField.Jtest line 119