OAI/Geometry/Convex/GeneralMahler/HMatrix.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

H_f, A, L from Equation (7) and their growth bounds
  1. def OAI.GeneralMahler.ProjField.kerH line 17
  2. def OAI.GeneralMahler.ProjField.Hmat line 18
  3. def OAI.GeneralMahler.ProjField.Amat line 19
  4. def OAI.GeneralMahler.ProjField.M line 20
  5. def OAI.GeneralMahler.ProjField.Lmat line 21
  6. def OAI.GeneralMahler.ProjField.Rmat line 22
  7. def OAI.GeneralMahler.ProjField.avgA line 23
  8. lemma OAI.GeneralMahler.ProjField.PD_herm line 24
  9. lemma OAI.GeneralMahler.ProjField.H_mixed line 29
  10. lemma OAI.GeneralMahler.ProjField.H_sm line 36
  11. lemma OAI.GeneralMahler.ProjField.H_ams line 40
  12. lemma OAI.GeneralMahler.ProjField.H_poly line 45
  13. lemma OAI.GeneralMahler.ProjField.H_left_int line 49
  14. lemma OAI.GeneralMahler.ProjField.H_SM line 53
  15. lemma OAI.GeneralMahler.ProjField.H_integrable line 56
  16. lemma OAI.GeneralMahler.ProjField.H_hermitian line 60
  17. lemma OAI.GeneralMahler.ProjField.poly_id_der line 64
  18. lemma OAI.GeneralMahler.ProjField.A_poly line 67
  19. lemma OAI.GeneralMahler.ProjField.A_SM line 69
  20. lemma OAI.GeneralMahler.ProjField.A_integrable line 70
  21. def OAI.GeneralMahler.ProjField.coord line 72
  22. lemma OAI.GeneralMahler.ProjField.coord_apply line 75
  23. lemma OAI.GeneralMahler.ProjField.A_coord_poly line 77
  24. lemma OAI.GeneralMahler.ProjField.A_coord_int line 80
  25. lemma OAI.GeneralMahler.ProjField.avgA_sym line 85
  26. lemma OAI.GeneralMahler.ProjField.M_sym line 88
  27. lemma OAI.GeneralMahler.ProjField.L_linear line 92
  28. lemma OAI.GeneralMahler.ProjField.L_poly line 98
  29. lemma OAI.GeneralMahler.ProjField.L_cont line 102
  30. lemma OAI.GeneralMahler.ProjField.L_sym line 105