OAI/Geometry/Convex/GeneralMahler/LogDet.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Normalized log determinant; derivative and simple growth estimates.

  1. def OAI.GeneralMahler.logD line 11
  2. def OAI.GeneralMahler.coeffMap line 12
  3. lemma OAI.GeneralMahler.det_cdiff line 18
  4. lemma OAI.GeneralMahler.D_log line 27
  5. lemma OAI.GeneralMahler.meas_logD line 29
  6. lemma OAI.GeneralMahler.perm_moves line 32
  7. lemma OAI.GeneralMahler.det_at_I_curve line 43
  8. lemma OAI.GeneralMahler.deriv_logD line 66
  9. lemma OAI.GeneralMahler.logD_sum line 79
  10. lemma OAI.GeneralMahler.logD_between line 86
  11. lemma OAI.GeneralMahler.logD_scalar line 104
  12. lemma OAI.GeneralMahler.trN_logD_eq line 109

    Source comment

    trace comparison for final connection
    lemma trN_logD_eq {A:Mat m} (ha:A.PosDef) :
    trN (cfc Real.log A)=logD A := by
…

    Mentions: OAI.GeneralMahler.Mat, OAI.GeneralMahler.trN, OAI.GeneralMahler.logD