OAI/Geometry/Convex/GeneralMahler/ScalarForm.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Integrating functionals; ext modulo constants.

  1. def OAI.GeneralMahler.ProjField.Iw line 14
  2. def OAI.GeneralMahler.ProjField.Idw line 15
  3. lemma OAI.GeneralMahler.ProjField.dm_e line 17
  4. lemma OAI.GeneralMahler.ProjField.Id_add line 21
  5. lemma OAI.GeneralMahler.ProjField.Id_sub line 25
  6. lemma OAI.GeneralMahler.ProjField.Id_cmul line 30
  7. lemma OAI.GeneralMahler.ProjField.Id_ext line 33
  8. lemma OAI.GeneralMahler.ProjField.L_ext line 36
  9. lemma OAI.GeneralMahler.ProjField.L_cmul line 55
  10. lemma OAI.GeneralMahler.ProjField.L_formula line 64
  11. lemma OAI.GeneralMahler.ProjField.delt_scale line 71
  12. lemma OAI.GeneralMahler.ProjField.ga_prod_comm line 78
  13. lemma OAI.GeneralMahler.ProjField.S0_e line 81