OAI/LinearAlgebra/MatrixFields/Entropy/InitialEntropy.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.PlacedInitial line 18
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.placement_read_card line 20
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.sum_placement_read line 24
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.initialShapeCode line 31
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.initialShapeCode_side line 34
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.rootShape_eq_initialShapeCode line 39
  7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.placedInitialLaw line 43
  8. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.orderedInitialLaw line 62
  9. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.nativeInitialMarginal line 65
  10. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.nativeH0 line 70
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.nativeInitialMarginal_eq_list line 72
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.sideMass_orderedInitialLaw line 81
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.orderedInitialLaw_sideMass line 99
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.nativeInitialMarginal_total line 125
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.nativeInitialMarginal_nonneg line 128
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.nativeH0_eq_finiteEntropy line 133
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.orderedInitialLaw_side_entropy line 136
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.ordinary_capacity_per_lot line 140
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.ordinary_capacity_all_lots line 151
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.population_cast_real line 160
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.initialJointCounts_cast line 167
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.initialJointCounts_ratio line 184
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropy.initialJointCounts_sideMass line 195