OAI/Geometry/Convex/GeneralMahler/GainFinal.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Combine the log-gains of the two matrices.

  1. def OAI.GeneralMahler.et line 13

    Source comment

    trace-and-expectation paper notation
    def et (A: Rn m→Mat m) := ∫ x,trN (A x) ∂normal m

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

  2. def OAI.GeneralMahler.etw line 14
  3. def OAI.GeneralMahler.eGain line 16
  4. def OAI.GeneralMahler.surplus line 17
  5. lemma OAI.GeneralMahler.eGain_exact line 19
  6. def OAI.GeneralMahler.eNt line 32
  7. lemma OAI.GeneralMahler.surplus_lower line 33
  8. def OAI.GeneralMahler.Edge.Plin line 45
  9. lemma OAI.GeneralMahler.Edge.pm_lin line 46
  10. lemma OAI.GeneralMahler.Edge.plSM line 51
  11. lemma OAI.GeneralMahler.Edge.lin_alt line 55
  12. lemma OAI.GeneralMahler.Edge.gain_alt line 65
  13. lemma OAI.GeneralMahler.Edge.h1_ref line 81
  14. lemma OAI.GeneralMahler.ProjField.vp_lin line 86
  15. lemma OAI.GeneralMahler.ProjField.gain_eq11 line 104