OAI/Probability/BinarySweep/Mixing/BinaryMixingBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.decay_eighth line 15
2. lemma OAI.BinaryCoordinateSweeps.centered_power_moment line 20
3. def OAI.BinaryCoordinateSweeps.binarySlotsFin line 51
4. lemma OAI.BinaryCoordinateSweeps.partition_slot_flat line 54
5. theorem OAI.BinaryCoordinateSweeps.binary_variation_bound_exists line 66
6. def OAI.BinaryCoordinateSweeps.BinaryMainTarget line 101
7. lemma OAI.BinaryCoordinateSweeps.binary_dimension_series_tendsto line 111
8. theorem OAI.BinaryCoordinateSweeps.constant_sweep_mixing line 118
9. theorem OAI.BinaryCoordinateSweeps.uniform_sweep_mixing line 135
10. theorem OAI.BinaryCoordinateSweeps.binary_main line 142