OAI/Geometry/Convex/GeneralMahler/BiWeight.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Layer functional ℒ and polynomial-growth calculus.

  1. structure OAI.GeneralMahler.Bwt line 12
  2. def OAI.GeneralMahler.bInt line 16
  3. def OAI.GeneralMahler.bAv line 17
  4. lemma OAI.GeneralMahler.Bwt.add line 21
  5. lemma OAI.GeneralMahler.Bwt.neg line 23
  6. lemma OAI.GeneralMahler.Bwt.sub line 24
  7. lemma OAI.GeneralMahler.Bwt.mul line 26
  8. lemma OAI.GeneralMahler.Bwt.fst line 28
  9. lemma OAI.GeneralMahler.Bwt.snd line 30
  10. lemma OAI.GeneralMahler.Bwt.const line 32
  11. lemma OAI.GeneralMahler.Bwt.bar line 33
  12. lemma OAI.GeneralMahler.Bwt.bar_eq line 58