OAI/Probability/SwitchChain/SlicePathComparison.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem315.SlicePathComparison.swaps line 15
2. theorem OAI.Problem315.SlicePathComparison.mem_swaps line 19
3. theorem OAI.Problem315.SlicePathComparison.variance_le_swap_squared_differences line 23
4. theorem OAI.Problem315.SlicePathComparison.relabel_displacement_eq_twice_energy line 46
5. theorem OAI.Problem315.SlicePathComparison.variance_le_card_sq_swap_energy line 56
6. theorem OAI.Problem315.SlicePathComparison.uniform_variance_le_card_sq_swap_energy line 73
7. theorem OAI.Problem315.SlicePathComparison.variance_le_card_sq_transport line 83