OAI/LinearAlgebra/MatrixMultiplication/Entropy/FloorExponentialRates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. def OAI.MatrixMultiplication.FloorExponentialRates.count line 16
  2. theorem OAI.MatrixMultiplication.FloorExponentialRates.count_pos line 18
  3. theorem OAI.MatrixMultiplication.FloorExponentialRates.log_count_bounds line 23
  4. theorem OAI.MatrixMultiplication.FloorExponentialRates.tendsto_log_count_div_nat line 39
  5. theorem OAI.MatrixMultiplication.FloorExponentialRates.tendsto_log_prod_count_div_nat line 56
  6. abbrev OAI.MatrixMultiplication.FloorExponentialRates.Labels line 68
  7. theorem OAI.MatrixMultiplication.FloorExponentialRates.card_labels line 70
  8. theorem OAI.MatrixMultiplication.FloorExponentialRates.card_labels_pos line 74
  9. theorem OAI.MatrixMultiplication.FloorExponentialRates.tendsto_log_card_labels_div_nat line 79