OAI/Probability/SwitchChain/FixedBlockMarginal.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.FixedBlockMarginal.average line 11
  2. theorem OAI.Problem315.FixedBlockMarginal.average_congr line 14
  3. theorem OAI.Problem315.FixedBlockMarginal.average_const line 20
  4. theorem OAI.Problem315.FixedBlockMarginal.average_equiv line 25
  5. theorem OAI.Problem315.FixedBlockMarginal.average_comm line 29
  6. theorem OAI.Problem315.FixedBlockMarginal.average_prod line 36
  7. theorem OAI.Problem315.FixedBlockMarginal.permutation_average_eq line 44
  8. theorem OAI.Problem315.FixedBlockMarginal.average_eq_permutation_average line 59
  9. theorem OAI.Problem315.FixedBlockMarginal.exists_perm_map line 79
  10. theorem OAI.Problem315.FixedBlockMarginal.average_row_eq line 97
  11. theorem OAI.Problem315.FixedBlockMarginal.row_function_average_eq line 117
  12. abbrev OAI.Problem315.FixedBlockMarginal.Subsets line 138
  13. def OAI.Problem315.FixedBlockMarginal.subsetPerm line 140
  14. theorem OAI.Problem315.FixedBlockMarginal.subsetPerm_mul line 153
  15. theorem OAI.Problem315.FixedBlockMarginal.subset_permutation_average_eq line 162
  16. theorem OAI.Problem315.FixedBlockMarginal.subset_average_eq_permutation_average line 179
  17. theorem OAI.Problem315.FixedBlockMarginal.average_row_eq_subset_average line 199
  18. theorem OAI.Problem315.FixedBlockMarginal.row_function_average_eq_subset_average line 210