OAI/LinearAlgebra/MatrixFields/Entropy/FloorExponentialRates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.FloorExponentialRates.count line 16
2. theorem OAI.MatrixAllFields.MatrixMultiplication.FloorExponentialRates.count_pos line 18
3. theorem OAI.MatrixAllFields.MatrixMultiplication.FloorExponentialRates.log_count_bounds line 23
4. theorem OAI.MatrixAllFields.MatrixMultiplication.FloorExponentialRates.tendsto_log_count_div_nat line 39
5. theorem OAI.MatrixAllFields.MatrixMultiplication.FloorExponentialRates.tendsto_log_prod_count_div_nat line 56
6. abbrev OAI.MatrixAllFields.MatrixMultiplication.FloorExponentialRates.Labels line 67
7. theorem OAI.MatrixAllFields.MatrixMultiplication.FloorExponentialRates.card_labels line 69
8. theorem OAI.MatrixAllFields.MatrixMultiplication.FloorExponentialRates.card_labels_pos line 73
9. theorem OAI.MatrixAllFields.MatrixMultiplication.FloorExponentialRates.tendsto_log_card_labels_div_nat line 78