OAI/Probability/SignedSweeps/TupleNorm.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedSweeps.firstRowStabilizer line 12
2. lemma OAI.SignedSweeps.firstRowStabilizer_fixes line 15
3. def OAI.SignedSweeps.restrictToTuple line 20
4. lemma OAI.SignedSweeps.restrictToTuple_apply line 23
5. lemma OAI.SignedSweeps.extendDifference_mem line 26
6. def OAI.SignedSweeps.permutationTupleEquiv line 36
7. lemma OAI.SignedSweeps.tupleRealization_norm_sq line 53
8. def OAI.SignedSweeps.tupleSweep line 68
9. lemma OAI.SignedSweeps.tupleRealization_intertwines_average line 72
10. lemma OAI.SignedSweeps.tupleRealization_intertwines_sweep line 79
11. theorem OAI.SignedSweeps.sweep_norm_le_of_tuple_bound line 94