OAI/Geometry/Convex/GeneralMahler/Inward.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A Brouwer inward estimate using spectral boxes directly for the transform B instead of round Frobenius balls in Q=log B. In particular the extreme eigenvectors alone suffice.

  1. lemma OAI.GeneralMahler.poly_cut line 14
  2. lemma OAI.GeneralMahler.inv_lim line 22
  3. lemma OAI.GeneralMahler.area_lim line 33
  4. theorem OAI.GeneralMahler.inward line 53