OAI/LinearAlgebra/MatrixMultiplication/Entropy/ComplexEntropyContinuity.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. theorem OAI.MatrixMultiplication.Foundation.entropyTerm_eq_negMulLog line 16
  2. theorem OAI.MatrixMultiplication.Foundation.entropyTerm_one line 18
  3. theorem OAI.MatrixMultiplication.Foundation.mul_entropyTerm_inv line 20
  4. theorem OAI.MatrixMultiplication.Foundation.finiteEntropy_uniform line 28
  5. theorem OAI.MatrixMultiplication.Foundation.finiteEntropy_deterministic line 34
  6. theorem OAI.MatrixMultiplication.Foundation.continuous_entropyTerm line 41
  7. theorem OAI.MatrixMultiplication.Foundation.entropyTerm_nonneg line 44
  8. theorem OAI.MatrixMultiplication.Foundation.concaveOn_entropyTerm line 48
  9. theorem OAI.MatrixMultiplication.Foundation.continuous_finiteEntropy line 51
  10. theorem OAI.MatrixMultiplication.Foundation.tendsto_entropyTerm line 57
  11. theorem OAI.MatrixMultiplication.Foundation.tendsto_entropyTerm_zero line 62
  12. theorem OAI.MatrixMultiplication.Foundation.tendsto_finiteEntropy_of_tendsto line 67
  13. theorem OAI.MatrixMultiplication.Foundation.finiteEntropy_nonneg line 73
  14. theorem OAI.MatrixMultiplication.Foundation.finiteEntropy_mix_le line 77
  15. theorem OAI.MatrixMultiplication.Foundation.finiteEntropy_le_log_card line 91
  16. def OAI.MatrixMultiplication.Foundation.FiniteLaw.uniform line 121
  17. theorem OAI.MatrixMultiplication.Foundation.FiniteLaw.uniform_mass line 129
  18. theorem OAI.MatrixMultiplication.Foundation.FiniteLaw.uniform_entropy line 132
  19. def OAI.MatrixMultiplication.Foundation.FiniteLaw.pure line 136
  20. theorem OAI.MatrixMultiplication.Foundation.FiniteLaw.pure_entropy line 143
  21. theorem OAI.MatrixMultiplication.Foundation.FiniteLaw.mass_le_one line 147
  22. theorem OAI.MatrixMultiplication.Foundation.FiniteLaw.entropy_nonneg line 153
  23. theorem OAI.MatrixMultiplication.Foundation.FiniteLaw.entropy_le_log_card line 156
  24. theorem OAI.MatrixMultiplication.Foundation.FiniteLaw.map_entropy_le line 160
  25. theorem OAI.MatrixMultiplication.Foundation.FiniteLaw.entropy_tendsto line 169