OAI/Geometry/Convex/GeneralMahler/Rigid/Axes.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Lipschitz/homogeneous with diagonal Jacobian a.e. ⇒ separate coordinates. Uses smoothG (gaussian averaging, §02).

  1. lemma OAI.GeneralMahler.lp_homo line 12
  2. lemma OAI.GeneralMahler.lp_same_smooth line 23
  3. lemma OAI.GeneralMahler.lp_mean_close line 43
  4. lemma OAI.GeneralMahler.lp_comp line 64