OAI/Probability/ThorpRouting/Harmonic/BlockProduct.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.sector_congr line 16
2. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.sector_factor_commute line 23
3. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.sector_projection line 28
4. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.sector_sum line 42
5. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.sector_absorb_factor line 67
6. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.sector_orthogonal line 83
7. def OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.blockProduct line 109
8. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.norm_noncommProd_le line 114
9. def OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.blocks line 124
10. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.blocks_norm_le_one line 128
11. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.blocks_sector_commute line 133
12. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.blocks_sector_norm line 147
13. def OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.coarse line 176
14. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.coarse_projection line 179
15. lemma OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.sector_coarse line 188
16. theorem OAI.ThorpNine.Harmonic.Thorp.CommutingBlocks.blocks_exception_bound line 206
17. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_weighted line 239
18. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_norm_le line 256
19. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_equiv line 262
20. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_prod line 268
21. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_inv line 280
22. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_palindrome line 285
23. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_one line 294
24. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_uniform line 300
25. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_uniform_mul line 304
26. def OAI.ThorpNine.Harmonic.Thorp.FiniteAverage.orderedProduct line 319
27. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteAverage.orderedProduct_eq line 323
28. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteAverage.multilinear_average line 339
29. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteAverage.ordered_average line 345
30. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteCharacters.character_expansion line 369
31. theorem OAI.ThorpNine.Harmonic.Thorp.FiniteCharacters.sum_dimension_sq line 396
32. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.averageMap_zero line 430
33. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.coefficient_cross_orthogonality line 439
34. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.regularAction line 457
35. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.regular_transitive line 463
36. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.regular_fixed line 468
37. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.regularCoefficient line 474
38. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.regularCoefficient_apply line 478
39. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.regularCoefficient_inner line 486
40. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.regularCoefficient_cross line 495
41. abbrev OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.CoefficientIndex line 527
42. def OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.coefficientFamily line 529
43. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.coefficientFamily_orthonormal line 534
44. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.coefficientIndex_card line 547
45. def OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.coefficientBasis line 551
46. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.coefficientBasis_apply line 556
47. theorem OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.parseval line 561
48. def OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.realVector line 567
49. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.coefficient_realVector line 570
50. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.coefficient_realVector_sq line 584
51. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.parseval_operator line 593
52. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.realVector_bound line 616
53. theorem OAI.ThorpNine.Harmonic.Thorp.FiniteFourier.l1_fourier_bound line 634
54. def OAI.ThorpNine.Harmonic.Thorp.ParallelBlocks.lift line 649
55. lemma OAI.ThorpNine.Harmonic.Thorp.ParallelBlocks.lift_apply line 658
56. def OAI.ThorpNine.Harmonic.Thorp.ParallelBlocks.injection line 660
57. lemma OAI.ThorpNine.Harmonic.Thorp.ParallelBlocks.injection_apply line 666
58. lemma OAI.ThorpNine.Harmonic.Thorp.ParallelBlocks.injection_commute line 671
59. lemma OAI.ThorpNine.Harmonic.Thorp.ParallelBlocks.lift_product line 680
60. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.continuousRepresentation_comp line 715
61. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_comp line 718
62. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.unitary_comp line 722
63. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_commute line 725
64. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_uniform_absorb line 737
65. lemma OAI.ThorpNine.Harmonic.Thorp.ParallelBlocks.local_average_commute line 750
66. lemma OAI.ThorpNine.Harmonic.Thorp.ParallelBlocks.sampleOperator_parallel line 759
67. def OAI.ThorpNine.Harmonic.Thorp.splitPerm line 784
68. def OAI.ThorpNine.Harmonic.Thorp.outerPerm line 787
69. lemma OAI.ThorpNine.Harmonic.Thorp.outerPerm_apply line 792
70. lemma OAI.ThorpNine.Harmonic.Thorp.splitPerm_butterfly line 795
71. lemma OAI.ThorpNine.Harmonic.Thorp.boundaryTree_node_raw line 807
72. lemma OAI.ThorpNine.Harmonic.Thorp.boundaryOutput_node_raw line 816
73. lemma OAI.ThorpNine.Harmonic.Thorp.boundaryTree_split line 822
74. lemma OAI.ThorpNine.Harmonic.Thorp.splitPerm_boundaryTree line 849
75. lemma OAI.ThorpNine.Harmonic.Thorp.boundaryOutput_split line 860
76. abbrev OAI.ThorpNine.Harmonic.Thorp.OuterCoins line 876
77. abbrev OAI.ThorpNine.Harmonic.Thorp.LocalCoins line 877
78. def OAI.ThorpNine.Harmonic.Thorp.parallelSplitCoinEquiv line 879
79. lemma OAI.ThorpNine.Harmonic.Thorp.parallelSplitCoinEquiv_apply line 884