OAI/LinearAlgebra/MatrixMultiplication/Entropy/LeafRates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. theorem OAI.MatrixMultiplication.LeafRates.log_card_supported line 17
  2. theorem OAI.MatrixMultiplication.LeafRates.log_card line 35
  3. theorem OAI.MatrixMultiplication.LeafRates.tendsto_log_card_supported line 43
  4. theorem OAI.MatrixMultiplication.LeafRates.tendsto_log_card line 69