OAI/Geometry/Convex/GeneralMahler/Matrix.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Matrix notation and ordered Euclidean operators used in §§02--06.

  1. abbrev OAI.GeneralMahler.Mat line 13
  2. abbrev OAI.GeneralMahler.op line 14
  3. def OAI.GeneralMahler.opCLE line 16
  4. lemma OAI.GeneralMahler.opCLE_apply line 19
  5. lemma OAI.GeneralMahler.opCLE_symm_apply line 20
  6. theorem OAI.GeneralMahler.op_norm line 22
  7. theorem OAI.GeneralMahler.continuous_op line 24
  8. theorem OAI.GeneralMahler.continuous_op_symm line 27
  9. lemma OAI.GeneralMahler.poly_op_apply line 30
  10. lemma OAI.GeneralMahler.op_inner_adjoint line 35
  11. lemma OAI.GeneralMahler.op_iff_hermitian line 40
  12. lemma OAI.GeneralMahler.op_posSemidef_iff line 53
  13. lemma OAI.GeneralMahler.op_posDef_iff line 66
  14. lemma OAI.GeneralMahler.op_order_iff line 80
  15. lemma OAI.GeneralMahler.le_one_norm line 85
  16. def OAI.GeneralMahler.opPair line 98

    Source documentation

    Realized paper expressions via clm evaluations.

    def opPair (x y : Rn n) : Mat n →L[ℝ] ℝ :=
…

    Mentions: OAI.GeneralMahler.Rn, OAI.GeneralMahler.Mat

  17. theorem OAI.GeneralMahler.opPair_apply line 101
  18. theorem OAI.GeneralMahler.op_inner_integral line 104
  19. theorem OAI.GeneralMahler.integral_opPair line 109
  20. theorem OAI.GeneralMahler.hermitian_integral line 116
  21. theorem OAI.GeneralMahler.psd_integral line 127
  22. def OAI.GeneralMahler.trN line 137

    Source documentation

    Normalized trace over coordinates.

    def trN (A : Mat n) := trace A / (n:ℝ)

    Mentions: OAI.GeneralMahler.Mat

  23. def OAI.GeneralMahler.trL line 139
  24. theorem OAI.GeneralMahler.trL_apply line 140