OAI/LinearAlgebra/MatrixMultiplication/Entropy/FiniteAverage.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. def OAI.MatrixMultiplication.PermutationMatching.average line 24
  2. theorem OAI.MatrixMultiplication.PermutationMatching.average_congr line 26
  3. theorem OAI.MatrixMultiplication.PermutationMatching.average_const line 32
  4. theorem OAI.MatrixMultiplication.PermutationMatching.average_zero line 38
  5. theorem OAI.MatrixMultiplication.PermutationMatching.average_add line 41
  6. theorem OAI.MatrixMultiplication.PermutationMatching.average_sub line 45
  7. theorem OAI.MatrixMultiplication.PermutationMatching.average_mul_const line 49
  8. theorem OAI.MatrixMultiplication.PermutationMatching.average_const_mul line 54
  9. theorem OAI.MatrixMultiplication.PermutationMatching.average_finset_sum line 59
  10. theorem OAI.MatrixMultiplication.PermutationMatching.average_sum line 65
  11. theorem OAI.MatrixMultiplication.PermutationMatching.average_nonneg line 69
  12. theorem OAI.MatrixMultiplication.PermutationMatching.average_mono line 72
  13. theorem OAI.MatrixMultiplication.PermutationMatching.average_indicator_eq line 77
  14. theorem OAI.MatrixMultiplication.PermutationMatching.average_equiv line 82
  15. theorem OAI.MatrixMultiplication.PermutationMatching.average_prod line 87
  16. theorem OAI.MatrixMultiplication.PermutationMatching.average_prod_average line 93
  17. theorem OAI.MatrixMultiplication.PermutationMatching.average_prod_fst line 99
  18. theorem OAI.MatrixMultiplication.PermutationMatching.average_prod_snd line 103
  19. theorem OAI.MatrixMultiplication.PermutationMatching.average_centered_sq line 107
  20. theorem OAI.MatrixMultiplication.PermutationMatching.average_pi_eval line 123
  21. theorem OAI.MatrixMultiplication.PermutationMatching.average_pi_restrict line 131
  22. theorem OAI.MatrixMultiplication.PermutationMatching.average_prod_pi_restrict line 141
  23. theorem OAI.MatrixMultiplication.PermutationMatching.average_pi_eval_mul line 157
  24. theorem OAI.MatrixMultiplication.PermutationMatching.average_pi_sum_centered_sq line 170
  25. theorem OAI.MatrixMultiplication.PermutationMatching.deviation_bound line 199
  26. theorem OAI.MatrixMultiplication.PermutationMatching.average_indicator_exists_le_sum line 212