OAI/Probability/SwitchChain/PermutationPoincare.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem315.PermutationPoincare.pull line 12
2. theorem OAI.Problem315.PermutationPoincare.pull_apply line 16
3. theorem OAI.Problem315.PermutationPoincare.norm_sq_eq_sum line 21
4. theorem OAI.Problem315.PermutationPoincare.norm_pull line 26
5. theorem OAI.Problem315.PermutationPoincare.displacement_mul_le line 33
6. theorem OAI.Problem315.PermutationPoincare.displacement_prod_le line 44
7. theorem OAI.Problem315.PermutationPoincare.sum_action_eq_zero line 61
8. theorem OAI.Problem315.PermutationPoincare.sum_displacement_sq line 86
9. theorem OAI.Problem315.PermutationPoincare.centered_norm_sq_le_of_bounded_words line 106