OAI/Geometry/Convex/GeneralMahler/EntScalar.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Entropy scalar simplification.

  1. lemma OAI.GeneralMahler.c_mul_p line 11
  2. lemma OAI.GeneralMahler.cR_v line 12
  3. lemma OAI.GeneralMahler.LC_average line 19
  4. lemma OAI.GeneralMahler.rapid_ca_prod line 39
  5. lemma OAI.GeneralMahler.rapid_wa line 42
  6. lemma OAI.GeneralMahler.int_wa line 45
  7. lemma OAI.GeneralMahler.wa_area line 47
  8. def OAI.GeneralMahler.ProjField.cBy line 57
  9. lemma OAI.GeneralMahler.ProjField.rapid_cdBy line 59
  10. lemma OAI.GeneralMahler.ProjField.i_wdB line 73
  11. lemma OAI.GeneralMahler.ProjField.i_ca_neg line 77
  12. lemma OAI.GeneralMahler.ProjField.cBy_eq line 80
  13. lemma OAI.GeneralMahler.ProjField.cost_eq line 105
  14. lemma OAI.GeneralMahler.ProjField.X_cost line 121
  15. lemma OAI.GeneralMahler.ProjField.Y_cost line 127