OAI/Probability/ThorpRouting/Harmonic/PairAssembleEquiv.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThorpNine.Harmonic.Thorp.pairAssembleEquiv line 11
2. def OAI.ThorpNine.Harmonic.Thorp.palindromeStageEquiv line 18
3. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeStageEquiv_apply line 23
4. def OAI.ThorpNine.Harmonic.Thorp.modifiedAssembleEquiv line 31
5. def OAI.ThorpNine.Harmonic.Thorp.modifiedStageEquiv line 39
6. lemma OAI.ThorpNine.Harmonic.Thorp.modifiedStageEquiv_apply line 45
7. lemma OAI.ThorpNine.Harmonic.Thorp.palindrome_stage line 54
8. def OAI.ThorpNine.Harmonic.Thorp.localModifiedPerm line 65
9. lemma OAI.ThorpNine.Harmonic.Thorp.modified_stage line 69
10. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_sandwich line 91
11. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.localModified_average line 98
12. lemma OAI.ThorpNine.Harmonic.Thorp.sampleOperator_palindrome_stage line 114
13. lemma OAI.ThorpNine.Harmonic.Thorp.sampleOperator_modified_stage line 130
14. def OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.retain line 155
15. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.retain_commute line 159
16. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.blocks_retain line 165
17. def OAI.ThorpNine.Harmonic.Thorp.ParallelBlocks.centralProjection line 189
18. lemma OAI.ThorpNine.Harmonic.Thorp.ParallelBlocks.centralProjection_commute line 193
19. lemma OAI.ThorpNine.Harmonic.Thorp.ParallelBlocks.local_central_commute line 199
20. lemma OAI.ThorpNine.Harmonic.Thorp.modified_central_average line 216
21. lemma OAI.ThorpNine.Harmonic.Thorp.central_local_gap line 229
22. lemma OAI.ThorpNine.Harmonic.Thorp.central_blocks_exception_bound line 236
23. theorem OAI.ThorpNine.Harmonic.Thorp.palindrome_exception_bound line 256
24. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.actionKernel line 279
25. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.actionKernel_apply line 283
26. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.randomOperator line 302
27. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.coefficient_random line 306
28. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.fixedSpace line 324
29. theorem OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.operator_amplification line 331
30. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.tupleAction line 364
31. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.tupleAction_apply line 374
32. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.tupleAction_transitive line 378
33. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.tupleAction_fixed_iff line 383
34. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.tupleAction_kernel line 394
35. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.irreducible_of_equiv line 406
36. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.unitaryRepresentation_coe line 423
37. def OAI.ThorpNine.Harmonic.Thorp.Specht.unitaryEquiv line 431
38. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.unitaryRepresentation_irreducible line 441
39. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.unitaryRepresentation_unitary line 446
40. def OAI.ThorpNine.Harmonic.Thorp.Specht.tupleFixedEquiv line 455
41. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.tupleFixed_dimension line 473
42. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_inv_apply line 490
43. theorem OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_amplification line 495
44. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.subrepresentationEquiv line 511
45. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.irreducible_comp_equiv line 527
46. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.relabelledUnitary_unitary line 539
47. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.relabelledUnitary_irreducible line 545
48. def OAI.ThorpNine.Harmonic.Thorp.Specht.relabelledTupleFixed line 550
49. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.relabelled_tuple_dimension line 584
50. def OAI.ThorpNine.Harmonic.Thorp.SparseContact.pointStabilizer line 596
51. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.swap_mem_pointStabilizer line 602
52. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.point_symmetrizer_zero line 607
53. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.point_fixed_zero line 639
54. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.point_unitary_fixed_zero line 651
55. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.point_relabelled_fixed_zero line 665
56. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.small_dominating_set line 685
57. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.powerset_weight_le_exp line 718
58. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.fixed_size_weight_le line 728
59. def OAI.ThorpNine.Harmonic.Thorp.SparseContact.neighborhood line 752
60. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.neighborhood_weight_le line 757
61. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.root_leaves_weight_le line 779
62. def OAI.ThorpNine.Harmonic.Thorp.SparseContact.NoIsolated line 802
63. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.small_dominating_subset line 805