OAI/Probability/BinarySweep/TensorBounds/EvenPostselection.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Density.reduced_postselection line 19
2. def OAI.BinaryCoordinateSweeps.Density.MatchedPair line 36
3. instance OAI.BinaryCoordinateSweeps.Density.(instance at line 37) line 37
4. instance OAI.BinaryCoordinateSweeps.Density.(instance at line 39) line 39
5. def OAI.BinaryCoordinateSweeps.Density.matchedEmbedding line 42
6. lemma OAI.BinaryCoordinateSweeps.Density.matchedEmbedding_injective line 45
7. def OAI.BinaryCoordinateSweeps.Density.pairVector line 48
8. lemma OAI.BinaryCoordinateSweeps.Density.reshape_pairVector line 52
9. def OAI.BinaryCoordinateSweeps.Density.wordPerm line 74
10. lemma OAI.BinaryCoordinateSweeps.Density.pairVector_symmetric line 81
11. theorem OAI.BinaryCoordinateSweeps.Density.even_block_postselection line 91
12. def OAI.BinaryCoordinateSweeps.Signed.signC line 124
13. lemma OAI.BinaryCoordinateSweeps.Signed.signC_one line 127
14. lemma OAI.BinaryCoordinateSweeps.Signed.signC_mul line 128
15. lemma OAI.BinaryCoordinateSweeps.Signed.signC_sq line 131
16. lemma OAI.BinaryCoordinateSweeps.Signed.signC_star line 136
17. lemma OAI.BinaryCoordinateSweeps.Signed.signC_swap line 138
18. def OAI.BinaryCoordinateSweeps.Signed.act line 143
19. lemma OAI.BinaryCoordinateSweeps.Signed.act_apply line 150
20. lemma OAI.BinaryCoordinateSweeps.Signed.act_one line 153
21. lemma OAI.BinaryCoordinateSweeps.Signed.act_mul line 157
22. def OAI.BinaryCoordinateSweeps.Signed.tensorRep line 171
23. def OAI.BinaryCoordinateSweeps.Signed.Invariant line 176
24. lemma OAI.BinaryCoordinateSweeps.Signed.invariant_same_parity line 180
25. lemma OAI.BinaryCoordinateSweeps.Signed.comp_swap_eq line 185
26. lemma OAI.BinaryCoordinateSweeps.Signed.invariant_repeated_mismatch_zero line 191
27. lemma OAI.BinaryCoordinateSweeps.Signed.invariant_mismatch_card line 210