OAI/LinearAlgebra/MatrixMultiplication/Entropy/ComplexOrientationRates.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. abbrev OAI.MatrixMultiplication.Foundation.OrientationRates.Orientation line 21
  2. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.orientation_card line 23
  3. def OAI.MatrixMultiplication.Foundation.OrientationRates.relativeOrientation line 27
  4. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.relativeOrientation_apply line 33
  5. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.unique_outer_orientation line 36
  6. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.sum_relative_orientation line 40
  7. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.prod_relative_orientation line 45
  8. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.site_population_in_orientation line 50
  9. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.histogram_in_original_orientation line 59
  10. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.target_multiplicity line 71
  11. def OAI.MatrixMultiplication.Foundation.OrientationRates.outputLaw line 79
  12. def OAI.MatrixMultiplication.Foundation.OrientationRates.affineScore line 83
  13. def OAI.MatrixMultiplication.Foundation.OrientationRates.totalNodeUtility line 86
  14. def OAI.MatrixMultiplication.Foundation.OrientationRates.totalCost line 89
  15. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.outputLaw_nonnegative line 94
  16. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.outputLaw_total line 102
  17. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.weighted_affineScore line 112
  18. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.weighted_affineScore_eq line 132
  19. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.totalCost_eq line 147
  20. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.utility_rate_identity line 157
  21. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.finite_utility_bound line 169
  22. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.log_resource_product line 188
  23. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.log_direct_multiplicity line 196
  24. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.raw_utility_accounting line 206
  25. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.physical_rate_normalization line 230
  26. theorem OAI.MatrixMultiplication.Foundation.OrientationRates.physical_cost_rate_identity line 254