OAI/Probability/CubeShuffle/UniformDecay.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubeShuffle.WeightedSweep.finite_positive_lower_bound line 11
2. lemma OAI.CubeShuffle.WeightedSweep.uniformOperator_zero_of_dimension_gt_one line 26
3. lemma OAI.CubeShuffle.WeightedSweep.dimension_full_row line 52
4. def OAI.CubeShuffle.WeightedSweep.localExponent line 64
5. lemma OAI.CubeShuffle.WeightedSweep.localExponent_pos line 67
6. lemma OAI.CubeShuffle.WeightedSweep.palindrome_local_bound line 72
7. theorem OAI.CubeShuffle.WeightedSweep.uniform_palindrome_dimension_decay line 101
8. theorem OAI.CubeShuffle.WeightedSweep.uniform_sweep_dimension_decay line 142