OAI/Geometry/Convex/GeneralMahler/Linear/Comm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

§06. Commuting normalization controls weighted norm.

  1. lemma OAI.GeneralMahler.sum_hsn line 12
  2. lemma OAI.GeneralMahler.H_J_frame line 21
  3. lemma OAI.GeneralMahler.Jgap_lower line 29
  4. lemma OAI.GeneralMahler.Jdev_upper line 44
  5. lemma OAI.GeneralMahler.commute_update line 65
  6. theorem OAI.GeneralMahler.Comm_bound line 77