OAI/Probability/ThorpRouting/SparseSaving/BlockProduct.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.sector_sum line 16
2. lemma OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.sector_absorb_factor line 41
3. lemma OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.sector_orthogonal line 57
4. def OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.blockProduct line 83
5. lemma OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.norm_noncommProd_le line 88
6. def OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.blocks line 98
7. lemma OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.blocks_norm_le_one line 102
8. lemma OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.blocks_sector_commute line 107
9. lemma OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.blocks_sector_norm line 121
10. def OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.coarse line 150
11. lemma OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.coarse_projection line 153
12. lemma OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.sector_coarse line 162
13. theorem OAI.ThorpNine.SparseSaving.Thorp.CommutingBlocks.blocks_exception_bound line 180
14. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_weighted line 213
15. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_norm_le line 230
16. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_equiv line 236
17. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_prod line 242
18. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_inv line 254
19. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_palindrome line 259
20. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_one line 268
21. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_uniform line 274
22. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_uniform_mul line 278
23. def OAI.ThorpNine.SparseSaving.Thorp.FiniteAverage.orderedProduct line 293
24. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteAverage.orderedProduct_eq line 297
25. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteAverage.multilinear_average line 313
26. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteAverage.ordered_average line 319
27. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteCharacters.character_expansion line 343
28. theorem OAI.ThorpNine.SparseSaving.Thorp.FiniteCharacters.sum_dimension_sq line 370
29. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.averageMap_zero line 404
30. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.coefficient_cross_orthogonality line 413
31. def OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.regularAction line 431
32. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.regular_transitive line 437
33. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.regular_fixed line 442
34. def OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.regularCoefficient line 448
35. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.regularCoefficient_apply line 452
36. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.regularCoefficient_inner line 460
37. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.regularCoefficient_cross line 469
38. abbrev OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.CoefficientIndex line 501
39. def OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.coefficientFamily line 503
40. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.coefficientFamily_orthonormal line 508
41. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.coefficientIndex_card line 521
42. def OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.coefficientBasis line 525
43. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.coefficientBasis_apply line 530
44. theorem OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.parseval line 535
45. def OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.realVector line 541
46. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.coefficient_realVector line 544
47. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.coefficient_realVector_sq line 558
48. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.parseval_operator line 567
49. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.realVector_bound line 590
50. theorem OAI.ThorpNine.SparseSaving.Thorp.FiniteFourier.l1_fourier_bound line 608
51. def OAI.ThorpNine.SparseSaving.Thorp.ParallelBlocks.lift line 623
52. lemma OAI.ThorpNine.SparseSaving.Thorp.ParallelBlocks.lift_apply line 632
53. def OAI.ThorpNine.SparseSaving.Thorp.ParallelBlocks.injection line 634
54. lemma OAI.ThorpNine.SparseSaving.Thorp.ParallelBlocks.injection_apply line 640
55. lemma OAI.ThorpNine.SparseSaving.Thorp.ParallelBlocks.injection_commute line 645
56. lemma OAI.ThorpNine.SparseSaving.Thorp.ParallelBlocks.lift_product line 654
57. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.continuousRepresentation_comp line 689
58. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_comp line 692
59. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.unitary_comp line 696
60. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_commute line 699
61. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.sampleOperator_uniform_absorb line 711
62. lemma OAI.ThorpNine.SparseSaving.Thorp.ParallelBlocks.local_average_commute line 724
63. lemma OAI.ThorpNine.SparseSaving.Thorp.ParallelBlocks.sampleOperator_parallel line 733
64. def OAI.ThorpNine.SparseSaving.Thorp.splitPerm line 758
65. def OAI.ThorpNine.SparseSaving.Thorp.outerPerm line 761
66. lemma OAI.ThorpNine.SparseSaving.Thorp.outerPerm_apply line 766
67. lemma OAI.ThorpNine.SparseSaving.Thorp.splitPerm_butterfly line 769
68. lemma OAI.ThorpNine.SparseSaving.Thorp.boundaryTree_node_raw line 781
69. lemma OAI.ThorpNine.SparseSaving.Thorp.boundaryOutput_node_raw line 790
70. lemma OAI.ThorpNine.SparseSaving.Thorp.boundaryTree_split line 796
71. lemma OAI.ThorpNine.SparseSaving.Thorp.splitPerm_boundaryTree line 823
72. lemma OAI.ThorpNine.SparseSaving.Thorp.boundaryOutput_split line 834
73. abbrev OAI.ThorpNine.SparseSaving.Thorp.OuterCoins line 850
74. abbrev OAI.ThorpNine.SparseSaving.Thorp.LocalCoins line 851
75. def OAI.ThorpNine.SparseSaving.Thorp.parallelSplitCoinEquiv line 853
76. lemma OAI.ThorpNine.SparseSaving.Thorp.parallelSplitCoinEquiv_apply line 858
77. def OAI.ThorpNine.SparseSaving.Thorp.pairAssembleEquiv line 862
78. def OAI.ThorpNine.SparseSaving.Thorp.palindromeStageEquiv line 869
79. lemma OAI.ThorpNine.SparseSaving.Thorp.palindromeStageEquiv_apply line 874
80. def OAI.ThorpNine.SparseSaving.Thorp.modifiedAssembleEquiv line 882