OAI/LinearAlgebra/MatrixFields/Entropy/FiniteAverage.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average line 18
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_congr line 20
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_const line 26
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_zero line 32
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_add line 35
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_sub line 39
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_mul_const line 43
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_const_mul line 48
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_finset_sum line 53
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_sum line 59
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_nonneg line 63
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_mono line 66
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_indicator_eq line 71
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_equiv line 76
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_prod line 81
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_prod_average line 87
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_prod_fst line 93
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_prod_snd line 97
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_centered_sq line 101
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_pi_eval line 117
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_pi_restrict line 125
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_prod_pi_restrict line 135
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_pi_eval_mul line 151
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_pi_sum_centered_sq line 164
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.deviation_bound line 193
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_indicator_exists_le_sum line 206