OAI/Probability/SwitchChain/SlicePermutationAction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem315.SlicePermutationAction.exists_perm_map_eq line 12
  2. abbrev OAI.Problem315.SlicePermutationAction.Slice line 23
  3. def OAI.Problem315.SlicePermutationAction.boundedSliceEquiv line 25
  4. def OAI.Problem315.SlicePermutationAction.relabel line 44
  5. theorem OAI.Problem315.SlicePermutationAction.relabel_one line 48
  6. theorem OAI.Problem315.SlicePermutationAction.relabel_mul line 56
  7. def OAI.Problem315.SlicePermutationAction.relabelEquiv line 64
  8. theorem OAI.Problem315.SlicePermutationAction.relabelEquiv_apply line 70
  9. def OAI.Problem315.SlicePermutationAction.relabelHom line 73
  10. theorem OAI.Problem315.SlicePermutationAction.sum_relabel line 78
  11. theorem OAI.Problem315.SlicePermutationAction.relabelEquiv_list_prod line 82
  12. def OAI.Problem315.SlicePermutationAction.mulAction line 86
  13. theorem OAI.Problem315.SlicePermutationAction.exists_relabel_eq line 91
  14. theorem OAI.Problem315.SlicePermutationAction.average_relabel_eq line 96
  15. theorem OAI.Problem315.SlicePermutationAction.average_relabel_sq_difference line 104