OAI/Probability/ThorpRouting/Adaptive/Representative.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.averageMap_self_trace line 14
2. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.averageMap_scalar line 23
3. theorem OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.coefficient_orthogonality line 34
4. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.representative line 59
5. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.representative_apply line 62
6. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.orbit_sum line 66
7. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.IsFixed line 86
8. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.coefficient line 88
9. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.coefficient_at line 92
10. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.coefficient_inner line 107
11. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.coefficient_action line 134
12. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.normalizedCoefficient line 142
13. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.normalizedCoefficient_inner line 145
14. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.normalizedCoefficient_orthonormal line 162
15. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.normalizedCoefficient_norm line 172
16. def OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.conv line 188
17. def OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.power line 189
18. lemma OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.conv_nonneg line 193
19. lemma OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.conv_pos_of line 196
20. lemma OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.sum_conv line 203
21. lemma OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.power_nonneg line 212
22. lemma OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.sum_power line 218
23. lemma OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.power_list_pos line 224
24. lemma OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.power_pos_mono line 233
25. theorem OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.exists_positive_power line 240
26. structure OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.Minorant line 255
27. def OAI.ThorpNine.Adaptive.Thorp.FiniteConvolution.minorant line 262
28. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.continuousRepresentation_apply line 287
29. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.unitary_norm line 291
30. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.continuousRepresentation_norm_le line 296
31. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.continuousRepresentation_adjoint line 303
32. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.weightedOperator line 311
33. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.weightedOperator_norm_le line 314
34. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.weightedOperator_symmetric line 322
35. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.uniformOperator line 332
36. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.uniformOperator_symmetric line 335
37. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.uniformOperator_left line 338
38. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.uniformOperator_right line 345
39. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.uniformOperator_idempotent line 352
40. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.uniformOperator_projection line 361
41. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.weighted_uniform_left line 365
42. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.weighted_uniform_right line 372
43. theorem OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.doeblin_off_invariants line 379
44. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.weightedOperator_conv line 414
45. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.weightedOperator_power line 427
46. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.off_invariants_pow line 433
47. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.minorantGap line 447
48. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.minorantGap_pos line 451
49. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.minorantGap_lt_one line 460
50. theorem OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.norm_off_invariants_le_gap line 464
51. def OAI.ThorpNine.Adaptive.Thorp.butterflyIdentity line 494
52. lemma OAI.ThorpNine.Adaptive.Thorp.pairSwitch_false line 498
53. lemma OAI.ThorpNine.Adaptive.Thorp.childLift_one line 504
54. lemma OAI.ThorpNine.Adaptive.Thorp.butterflyIdentity_perm line 508
55. def OAI.ThorpNine.Adaptive.Thorp.childInjection line 513
56. lemma OAI.ThorpNine.Adaptive.Thorp.childInjection_swap line 522
57. lemma OAI.ThorpNine.Adaptive.Thorp.pairSwitch_single line 542
58. theorem OAI.ThorpNine.Adaptive.Thorp.butterfly_generates line 555
59. lemma OAI.ThorpNine.Adaptive.Thorp.butterfly_closure line 595
60. def OAI.ThorpNine.Adaptive.Thorp.sampleLaw line 600
61. lemma OAI.ThorpNine.Adaptive.Thorp.sampleLaw_nonneg line 604
62. lemma OAI.ThorpNine.Adaptive.Thorp.sampleLaw_sum line 607
63. lemma OAI.ThorpNine.Adaptive.Thorp.sampleLaw_pos_iff line 613
64. lemma OAI.ThorpNine.Adaptive.Thorp.sampleLaw_equiv line 624
65. lemma OAI.ThorpNine.Adaptive.Thorp.sampleLaw_inverse line 632
66. lemma OAI.ThorpNine.Adaptive.Thorp.sampleLaw_symmetric line 639
67. lemma OAI.ThorpNine.Adaptive.Thorp.palindrome_identity line 650
68. lemma OAI.ThorpNine.Adaptive.Thorp.palindrome_range_contains_butterfly line 655
69. lemma OAI.ThorpNine.Adaptive.Thorp.palindrome_support_generates line 663
70. def OAI.ThorpNine.Adaptive.Thorp.palindromeMinorant line 670
71. def OAI.ThorpNine.Adaptive.Thorp.blockGap line 675
72. lemma OAI.ThorpNine.Adaptive.Thorp.blockGap_pos line 677
73. lemma OAI.ThorpNine.Adaptive.Thorp.blockGap_lt_one line 678
74. theorem OAI.ThorpNine.Adaptive.Thorp.palindrome_off_invariants_gap line 680
75. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.orthogonal_sum_norm_sq line 696
76. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.projection_inner_zero line 709
77. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.projection_sandwich_norm line 716
78. theorem OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.resolution_norm_bound line 725
79. theorem OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.sector_sandwich_le line 753
80. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.resolution_commute line 775
81. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.resolution_sum_mul line 782
82. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.resolution_truncated_norm line 792
83. theorem OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.resolution_exception_bound line 807
84. def OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.choice line 841
85. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.choice_commute line 846
86. def OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.sector line 855
87. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.sector_insert line 859
88. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.sector_congr line 864
89. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.sector_factor_commute line 871
90. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.sector_projection line 876