OAI/Probability/ThorpRouting/Casimir/AverageMap.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.averageMap line 14
2. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.averageMap_self_trace line 30
3. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.averageMap_scalar line 39
4. theorem OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.coefficient_orthogonality line 50
5. def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.representative line 75
6. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.representative_apply line 78
7. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.orbit_sum line 82
8. def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.IsFixed line 102
9. def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.coefficient line 104
10. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.coefficient_at line 108
11. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.coefficient_inner line 123
12. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.coefficient_action line 150
13. def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.normalizedCoefficient line 158
14. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.normalizedCoefficient_inner line 161
15. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.normalizedCoefficient_orthonormal line 178
16. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.normalizedCoefficient_norm line 188
17. def OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.conv line 204
18. def OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.power line 205
19. lemma OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.conv_nonneg line 209
20. lemma OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.conv_pos_of line 212
21. lemma OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.sum_conv line 219
22. lemma OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.power_nonneg line 228
23. lemma OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.sum_power line 234
24. lemma OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.power_list_pos line 240
25. lemma OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.power_pos_mono line 249
26. theorem OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.exists_positive_power line 256
27. structure OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.Minorant line 271
28. def OAI.ThorpNine.Casimir.Thorp.FiniteConvolution.minorant line 278
29. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.continuousRepresentation_apply line 303
30. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.unitary_norm line 307
31. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.continuousRepresentation_norm_le line 312
32. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.continuousRepresentation_adjoint line 319
33. def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.weightedOperator line 327
34. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.weightedOperator_norm_le line 330
35. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.weightedOperator_symmetric line 338
36. def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.uniformOperator line 348
37. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.uniformOperator_symmetric line 351
38. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.uniformOperator_left line 354
39. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.uniformOperator_right line 361
40. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.uniformOperator_idempotent line 368
41. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.uniformOperator_projection line 377
42. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.weighted_uniform_left line 381
43. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.weighted_uniform_right line 388
44. theorem OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.doeblin_off_invariants line 395
45. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.weightedOperator_conv line 430
46. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.weightedOperator_power line 443
47. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.off_invariants_pow line 449
48. def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.minorantGap line 463
49. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.minorantGap_pos line 467
50. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.minorantGap_lt_one line 476
51. theorem OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.norm_off_invariants_le_gap line 480
52. def OAI.ThorpNine.Casimir.Thorp.butterflyIdentity line 510
53. lemma OAI.ThorpNine.Casimir.Thorp.pairSwitch_false line 514
54. lemma OAI.ThorpNine.Casimir.Thorp.childLift_one line 520
55. lemma OAI.ThorpNine.Casimir.Thorp.butterflyIdentity_perm line 524
56. def OAI.ThorpNine.Casimir.Thorp.childInjection line 529
57. lemma OAI.ThorpNine.Casimir.Thorp.childInjection_swap line 538
58. lemma OAI.ThorpNine.Casimir.Thorp.pairSwitch_single line 558
59. theorem OAI.ThorpNine.Casimir.Thorp.butterfly_generates line 571
60. lemma OAI.ThorpNine.Casimir.Thorp.butterfly_closure line 611
61. def OAI.ThorpNine.Casimir.Thorp.sampleLaw line 616
62. lemma OAI.ThorpNine.Casimir.Thorp.sampleLaw_nonneg line 620
63. lemma OAI.ThorpNine.Casimir.Thorp.sampleLaw_sum line 623
64. lemma OAI.ThorpNine.Casimir.Thorp.sampleLaw_pos_iff line 629
65. lemma OAI.ThorpNine.Casimir.Thorp.sampleLaw_equiv line 640
66. lemma OAI.ThorpNine.Casimir.Thorp.sampleLaw_inverse line 648
67. lemma OAI.ThorpNine.Casimir.Thorp.sampleLaw_symmetric line 655
68. lemma OAI.ThorpNine.Casimir.Thorp.palindrome_identity line 666
69. lemma OAI.ThorpNine.Casimir.Thorp.palindrome_range_contains_butterfly line 671
70. lemma OAI.ThorpNine.Casimir.Thorp.palindrome_support_generates line 679
71. def OAI.ThorpNine.Casimir.Thorp.palindromeMinorant line 686
72. def OAI.ThorpNine.Casimir.Thorp.blockGap line 691
73. lemma OAI.ThorpNine.Casimir.Thorp.blockGap_pos line 693
74. lemma OAI.ThorpNine.Casimir.Thorp.blockGap_lt_one line 694
75. theorem OAI.ThorpNine.Casimir.Thorp.palindrome_off_invariants_gap line 696
76. lemma OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.orthogonal_sum_norm_sq line 712
77. lemma OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.projection_inner_zero line 725
78. lemma OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.projection_sandwich_norm line 732
79. theorem OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.resolution_norm_bound line 741
80. theorem OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.sector_sandwich_le line 769
81. lemma OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.resolution_commute line 791
82. lemma OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.resolution_sum_mul line 798
83. lemma OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.resolution_truncated_norm line 808
84. theorem OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.resolution_exception_bound line 823
85. def OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.choice line 857
86. lemma OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.choice_commute line 862
87. def OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.sector line 871
88. lemma OAI.ThorpNine.Casimir.Thorp.CommutingBlocks.sector_insert line 875