OAI/Probability/SwitchChain/PermutationPathComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.PermutationPaths.path_squared_difference_le line 10
2. theorem OAI.Problem315.PermutationPaths.permutation_path_energy_le line 28
3. theorem OAI.Problem315.PermutationPaths.sum_group_apply_eq line 62
4. theorem OAI.Problem315.PermutationPaths.sum_pairwise_sq_eq line 87
5. theorem OAI.Problem315.PermutationPaths.sum_group_squared_difference_eq line 114
6. theorem OAI.Problem315.PermutationPaths.variance_le_generator_energy line 136
7. theorem OAI.Problem315.PermutationPaths.exists_path_of_word line 173
8. theorem OAI.Problem315.PermutationPaths.variance_le_generator_energy_of_words line 198