OAI/RepresentationTheory/SpinAngle/Core.lean

GitHub source file

445 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SpinAngle.Specht.cyclic line 16

    Also declared: ComparatorChallenges/SpinAngle.lean:16 (same declaration text).

  2. lemma OAI.SpinAngle.Specht.self_mem_cyclic line 30
  3. lemma OAI.SpinAngle.Specht.starProjection_rep line 36
  4. theorem OAI.SpinAngle.Specht.simple_eigen_submodule_alternative line 54
  5. theorem OAI.SpinAngle.Specht.cyclic_irreducible_of_simple_eigen line 94
  6. def OAI.SpinAngle.TensorRep.tensor line 140

    Also declared: ComparatorChallenges/SpinAngle.lean:35 (same declaration text).

  7. lemma OAI.SpinAngle.TensorRep.tensor_star line 143
  8. lemma OAI.SpinAngle.TensorRep.tensor_mul line 153

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:38 (different declaration text). Qualify references as OAI.SpinAngle.TensorRep.tensor_mul@path.

  9. lemma OAI.SpinAngle.TensorRep.tensor_one line 166

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:51 (different declaration text). Qualify references as OAI.SpinAngle.TensorRep.tensor_one@path.

  10. lemma OAI.SpinAngle.TensorRep.tensor_diagonal line 182
  11. lemma OAI.SpinAngle.TensorRep.toEuclideanLin_mul line 199

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:67 (different declaration text). Qualify references as OAI.SpinAngle.TensorRep.toEuclideanLin_mul@path.

  12. lemma OAI.SpinAngle.TensorRep.toEuclideanLin_one line 211

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:79 (different declaration text). Qualify references as OAI.SpinAngle.TensorRep.toEuclideanLin_one@path.

  13. def OAI.SpinAngle.TensorRep.action line 222

    Also declared: ComparatorChallenges/SpinAngle.lean:89 (same declaration text).

  14. def OAI.SpinAngle.TensorRep.rep line 229

    Also declared: ComparatorChallenges/SpinAngle.lean:94 (same declaration text).

  15. lemma OAI.SpinAngle.TensorRep.tensor_mem_unitary line 232
  16. lemma OAI.SpinAngle.TensorRep.toEuclideanLin_unitary line 240
  17. lemma OAI.SpinAngle.TensorRep.rep_unitary line 249
  18. lemma OAI.SpinAngle.TensorRep.tensor_reindex line 254

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:97 (different declaration text). Qualify references as OAI.SpinAngle.TensorRep.tensor_reindex@path.

  19. lemma OAI.SpinAngle.TensorRep.action_diagonal line 264
  20. def OAI.SpinAngle.Specht.PermutationSpace.rep line 282

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:116 (same statement text; different proof or body). Qualify references as OAI.SpinAngle.Specht.PermutationSpace.rep@path.

  21. lemma OAI.SpinAngle.Specht.PermutationSpace.rep_apply line 295
  22. lemma OAI.SpinAngle.Specht.PermutationSpace.rep_unitary line 298
  23. lemma OAI.SpinAngle.Specht.PermutationSpace.rep_single line 304
  24. def OAI.SpinAngle.Specht.PermutationSpace.alternator line 314

    Also declared: ComparatorChallenges/SpinAngle.lean:130 (same declaration text).

  25. lemma OAI.SpinAngle.Specht.PermutationSpace.alternator_apply line 318

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:134 (same statement text; different proof or body). Qualify references as OAI.SpinAngle.Specht.PermutationSpace.alternator_apply@path.

  26. lemma OAI.SpinAngle.Specht.PermutationSpace.alternator_stable line 323
  27. lemma OAI.SpinAngle.Specht.PermutationSpace.alternator_translate line 330
  28. lemma OAI.SpinAngle.Specht.PermutationSpace.alternator_single_zero line 347
  29. lemma OAI.SpinAngle.Specht.PermutationSpace.alternator_coeff line 358
  30. lemma OAI.SpinAngle.Specht.PermutationSpace.polytabloid_base line 363
  31. lemma OAI.SpinAngle.Specht.PermutationSpace.polytabloid_inner line 377
  32. theorem OAI.SpinAngle.Specht.PermutationSpace.alternator_rank_one line 390
  33. def OAI.SpinAngle.Specht.complexSign line 423

    Also declared: ComparatorChallenges/SpinAngle.lean:162 (same declaration text).

  34. lemma OAI.SpinAngle.Specht.complexSign_conj line 428
  35. lemma OAI.SpinAngle.Specht.complexSign_inv line 431

    Also declared: ComparatorChallenges/SpinAngle.lean:167 (same declaration text).

  36. lemma OAI.SpinAngle.Specht.complexSign_swap line 434
  37. abbrev OAI.SpinAngle.Young.Cells line 442

    Also declared: ComparatorChallenges/SpinAngle.lean:174 (same declaration text).

  38. lemma OAI.SpinAngle.Young.fin_le_strictMono line 444
  39. lemma OAI.SpinAngle.Young.card_column line 458
  40. lemma OAI.SpinAngle.Young.card_row_subtype line 471
  41. lemma OAI.SpinAngle.Young.eq_of_rowPreserving line 482
  42. theorem OAI.SpinAngle.Young.column_sort_le line 496
  43. lemma OAI.SpinAngle.Young.rowRankSum_le line 539
  44. theorem OAI.SpinAngle.Young.column_sort line 546
  45. instance OAI.SpinAngle.PolynomialCarrier.coloringAction line 567

    Also declared: ComparatorChallenges/SpinAngle.lean:183 (same declaration text).

  46. lemma OAI.SpinAngle.PolynomialCarrier.site_apply line 572
  47. def OAI.SpinAngle.PolynomialCarrier.reindex line 580

    Also declared: ComparatorChallenges/SpinAngle.lean:188 (same declaration text).

  48. lemma OAI.SpinAngle.PolynomialCarrier.action_site_commute line 586

    Also declared: ComparatorChallenges/SpinAngle.lean:194 (same declaration text).

  49. def OAI.SpinAngle.PolynomialCarrier.columnGroup line 601

    Also declared: ComparatorChallenges/SpinAngle.lean:208 (same declaration text).

  50. abbrev OAI.SpinAngle.PolynomialCarrier.TensorSpace line 610

    Also declared: ComparatorChallenges/SpinAngle.lean:217 (same declaration text).

  51. def OAI.SpinAngle.PolynomialCarrier.alternating line 614

    Also declared: ComparatorChallenges/SpinAngle.lean:219 (same declaration text).

  52. def OAI.SpinAngle.PolynomialCarrier.rowColor line 629

    Also declared: ComparatorChallenges/SpinAngle.lean:234 (same declaration text).

  53. def OAI.SpinAngle.PolynomialCarrier.highest line 634

    Also declared: ComparatorChallenges/SpinAngle.lean:239 (same declaration text).

  54. lemma OAI.SpinAngle.PolynomialCarrier.rowColor_column_free line 640
  55. lemma OAI.SpinAngle.PolynomialCarrier.highest_base line 659
  56. lemma OAI.SpinAngle.PolynomialCarrier.highest_ne_zero line 666
  57. lemma OAI.SpinAngle.Specht.PermutationSpace.rep_alternator line 676

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:138 (different declaration text). Qualify references as OAI.SpinAngle.Specht.PermutationSpace.rep_alternator@path.

  58. lemma OAI.SpinAngle.PolynomialCarrier.highest_mem line 702

    Also declared: ComparatorChallenges/SpinAngle.lean:245 (same declaration text).

  59. lemma OAI.SpinAngle.PolynomialCarrier.alternating_collision line 713
  60. lemma OAI.SpinAngle.PolynomialCarrier.alternating_injective line 740
  61. lemma OAI.SpinAngle.PolynomialCarrier.alternating_minimal_weight line 749
  62. lemma OAI.SpinAngle.PolynomialCarrier.diagonal_single line 788
  63. lemma OAI.SpinAngle.PolynomialCarrier.diagonal_unitary line 798
  64. def OAI.SpinAngle.PolynomialCarrier.weightOrder line 812
  65. def OAI.SpinAngle.PolynomialCarrier.weightRoot line 814
  66. lemma OAI.SpinAngle.PolynomialCarrier.weightRoot_primitive line 816
  67. lemma OAI.SpinAngle.PolynomialCarrier.weightRoot_unitary line 819
  68. def OAI.SpinAngle.PolynomialCarrier.weightElement line 825
  69. lemma OAI.SpinAngle.PolynomialCarrier.weight_sum_lt line 828
  70. lemma OAI.SpinAngle.PolynomialCarrier.weight_action line 835
  71. lemma OAI.SpinAngle.PolynomialCarrier.highest_diagonal line 840
  72. lemma OAI.SpinAngle.PolynomialCarrier.highest_weight_eigen line 850
  73. lemma OAI.SpinAngle.PolynomialCarrier.weight_eigen_support line 859
  74. theorem OAI.SpinAngle.PolynomialCarrier.weight_eigenspace_one_dimensional line 872
  75. def OAI.SpinAngle.PolynomialCarrier.ordinary line 891

    Also declared: ComparatorChallenges/SpinAngle.lean:255 (same declaration text).

  76. theorem OAI.SpinAngle.PolynomialCarrier.ordinary_irreducible line 895
  77. lemma OAI.SpinAngle.TensorRep.diagonal_unitary_of_star_mul line 916
  78. lemma OAI.SpinAngle.TensorRep.diagonal_single line 927
  79. def OAI.SpinAngle.TensorRep.content line 937
  80. lemma OAI.SpinAngle.TensorRep.product_content line 939
  81. lemma OAI.SpinAngle.TensorRep.phase_product line 949
  82. lemma OAI.SpinAngle.TensorRep.content_le_card line 959
  83. lemma OAI.SpinAngle.TensorRep.intertwiner_content_zero line 969
  84. lemma OAI.SpinAngle.TensorRep.intertwiner_diagonal line 995
  85. lemma OAI.SpinAngle.TensorRep.intertwiner_hermitian line 1022
  86. lemma OAI.SpinAngle.TensorRep.apply_mem_hermitian line 1041
  87. def OAI.SpinAngle.PolynomialCarrier.highestMonomial line 1066
  88. lemma OAI.SpinAngle.PolynomialCarrier.highestMonomial_nonneg line 1068
  89. lemma OAI.SpinAngle.PolynomialCarrier.monomial_le_highest line 1073
  90. theorem OAI.SpinAngle.PolynomialCarrier.diagonal_norm_bound line 1085
  91. def OAI.SpinAngle.SortedSpectrum.values line 1113
  92. def OAI.SpinAngle.SortedSpectrum.basis line 1116
  93. def OAI.SpinAngle.SortedSpectrum.changeBasis line 1119
  94. lemma OAI.SpinAngle.SortedSpectrum.changeBasis_apply line 1123
  95. lemma OAI.SpinAngle.SortedSpectrum.values_antitone line 1125
  96. lemma OAI.SpinAngle.SortedSpectrum.eigenvector line 1128
  97. lemma OAI.SpinAngle.SortedSpectrum.spectral_theorem line 1132
  98. lemma OAI.SpinAngle.SortedSpectrum.values_nonneg line 1144
  99. lemma OAI.SpinAngle.SortedSpectrum.trace_eq_sum line 1150
  100. abbrev OAI.SpinAngle.PolynomialCarrier.Carrier line 1162

    Also declared: ComparatorChallenges/SpinAngle.lean:259 (same declaration text).

  101. instance OAI.SpinAngle.PolynomialCarrier.carrierInner line 1164

    Also declared: ComparatorChallenges/SpinAngle.lean:261 (same declaration text).

  102. def OAI.SpinAngle.PolynomialCarrier.inclusion line 1169
  103. lemma OAI.SpinAngle.PolynomialCarrier.inclusion_apply line 1172
  104. lemma OAI.SpinAngle.PolynomialCarrier.inclusion_equivariant line 1174
  105. def OAI.SpinAngle.PolynomialCarrier.image line 1178
  106. lemma OAI.SpinAngle.PolynomialCarrier.inclusion_image line 1184
  107. def OAI.SpinAngle.PolynomialCarrier.hermitianAction line 1187
  108. lemma OAI.SpinAngle.PolynomialCarrier.inclusion_hermitianAction line 1193
  109. lemma OAI.SpinAngle.PolynomialCarrier.tensor_hermitian line 1199
  110. lemma OAI.SpinAngle.PolynomialCarrier.hermitianAction_symmetric line 1207
  111. lemma OAI.SpinAngle.PolynomialCarrier.ordinary_rep_unitary line 1214
  112. lemma OAI.SpinAngle.PolynomialCarrier.raw_norm_unitary line 1218
  113. theorem OAI.SpinAngle.PolynomialCarrier.hermitianAction_norm_bound line 1223
  114. def OAI.SpinAngle.ExternalTensor.rep line 1257

    Also declared: ComparatorChallenges/SpinAngle.lean:274 (same declaration text).

  115. lemma OAI.SpinAngle.ExternalTensor.rep_tmul line 1261
  116. def OAI.SpinAngle.ExternalTensor.rightSlice line 1275
  117. def OAI.SpinAngle.ExternalTensor.leftSlice line 1278
  118. lemma OAI.SpinAngle.ExternalTensor.rightSlice_tmul line 1281
  119. lemma OAI.SpinAngle.ExternalTensor.leftSlice_tmul line 1290
  120. lemma OAI.SpinAngle.ExternalTensor.slice_commute line 1300
  121. lemma OAI.SpinAngle.ExternalTensor.slice_map_left line 1313
  122. lemma OAI.SpinAngle.ExternalTensor.eq_sum_slices line 1326
  123. lemma OAI.SpinAngle.ExternalTensor.rightSlice_ext line 1341
  124. lemma OAI.SpinAngle.ExternalTensor.scalar_of_commute line 1348
  125. lemma OAI.SpinAngle.ExternalTensor.left_commutant line 1359
  126. lemma OAI.SpinAngle.ExternalTensor.commutant_scalar line 1388
  127. lemma OAI.SpinAngle.ExternalTensor.unitary line 1413
  128. lemma OAI.SpinAngle.ExternalTensor.projection_commute line 1432
  129. theorem OAI.SpinAngle.ExternalTensor.irreducible line 1449
  130. lemma OAI.SpinAngle.TorusNaturality.repr_diagonal line 1511
  131. lemma OAI.SpinAngle.TorusNaturality.coefficient_zero line 1521
  132. theorem OAI.SpinAngle.TorusNaturality.diagonal line 1567
  133. abbrev OAI.SpinAngle.SignedTensor.Spin line 1590

    Also declared: ComparatorChallenges/SpinAngle.lean:284 (same declaration text).

  134. abbrev OAI.SpinAngle.SignedTensor.Mat line 1591

    Also declared: ComparatorChallenges/SpinAngle.lean:285 (same declaration text).

  135. abbrev OAI.SpinAngle.SignedTensor.Group line 1592

    Also declared: ComparatorChallenges/SpinAngle.lean:286 (same declaration text).

  136. def OAI.SpinAngle.SignedTensor.block line 1594

    Also declared: ComparatorChallenges/SpinAngle.lean:288 (same declaration text).

  137. lemma OAI.SpinAngle.SignedTensor.block_star line 1607

    Also declared: ComparatorChallenges/SpinAngle.lean:301 (same declaration text).

  138. def OAI.SpinAngle.SignedTensor.blockGroup line 1614

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:308 (same statement text; different proof or body). Qualify references as OAI.SpinAngle.SignedTensor.blockGroup@path.

  139. abbrev OAI.SpinAngle.SignedTensor.Raw line 1633

    Also declared: ComparatorChallenges/SpinAngle.lean:327 (same declaration text).

  140. abbrev OAI.SpinAngle.SignedTensor.PairRaw line 1634
  141. def OAI.SpinAngle.SignedTensor.rep line 1636

    Also declared: ComparatorChallenges/SpinAngle.lean:329 (same declaration text).

  142. def OAI.SpinAngle.SignedTensor.pairRep line 1639
  143. def OAI.SpinAngle.SignedTensor.pairAction line 1642
  144. lemma OAI.SpinAngle.SignedTensor.pairAction_tmul line 1656
  145. lemma OAI.SpinAngle.SignedTensor.pairRep_eq line 1660
  146. lemma OAI.SpinAngle.SignedTensor.rep_unitary line 1662
  147. lemma OAI.SpinAngle.SignedTensor.pairRep_unitary line 1665
  148. def OAI.SpinAngle.SignedTensor.pairBasis line 1670
  149. def OAI.SpinAngle.SignedTensor.pairContent line 1673
  150. def OAI.SpinAngle.SignedTensor.diagPair line 1676
  151. lemma OAI.SpinAngle.SignedTensor.block_diagPair line 1679
  152. lemma OAI.SpinAngle.SignedTensor.pairBasis_diagonal line 1686
  153. theorem OAI.SpinAngle.SignedTensor.intertwiner_diagonal line 1700
  154. lemma OAI.SpinAngle.SignedTensor.pair_spectral line 1719
  155. theorem OAI.SpinAngle.SignedTensor.intertwiner_hermitian line 1730
  156. lemma OAI.SpinAngle.UnitaryNaturality.inner_move line 1761
  157. lemma OAI.SpinAngle.UnitaryNaturality.adjoint_intertwines line 1775
  158. lemma OAI.SpinAngle.UnitaryNaturality.adjoint_isometry line 1783
  159. abbrev OAI.SpinAngle.SignedCarrier.Carrier line 1797

    Also declared: ComparatorChallenges/SpinAngle.lean:372 (same declaration text).

  160. instance OAI.SpinAngle.SignedCarrier.carrierNormed line 1799

    Also declared: ComparatorChallenges/SpinAngle.lean:374 (same declaration text).

  161. instance OAI.SpinAngle.SignedCarrier.carrierInner line 1803

    Also declared: ComparatorChallenges/SpinAngle.lean:378 (same declaration text).

  162. instance OAI.SpinAngle.SignedCarrier.carrierFinite line 1807

    Also declared: ComparatorChallenges/SpinAngle.lean:382 (same declaration text).

  163. abbrev OAI.SpinAngle.SignedCarrier.rep line 1810

    Also declared: ComparatorChallenges/SpinAngle.lean:385 (same declaration text).

  164. instance OAI.SpinAngle.SignedCarrier.irreducible line 1815
  165. def OAI.SpinAngle.SignedCarrier.inclusion line 1820
  166. lemma OAI.SpinAngle.SignedCarrier.inclusion_equivariant line 1825
  167. lemma OAI.SpinAngle.SignedCarrier.rep_unitary line 1832
  168. def OAI.SpinAngle.SignedCarrier.hermitianAction line 1839
  169. lemma OAI.SpinAngle.SignedCarrier.inclusion_hermitianAction line 1844
  170. theorem OAI.SpinAngle.SignedCarrier.intertwiner_hermitian line 1862
  171. lemma OAI.SpinAngle.TensorRep.continuous_action line 1889
  172. lemma OAI.SpinAngle.TensorRep.continuous_rep line 1896
  173. lemma OAI.SpinAngle.PolynomialCarrier.continuous_rep line 1906
  174. lemma OAI.SpinAngle.ExternalTensor.continuous_rep line 1923
  175. lemma OAI.SpinAngle.SignedTensor.continuous_block line 1945
  176. lemma OAI.SpinAngle.SignedTensor.continuous_blockGroup line 1955
  177. lemma OAI.SpinAngle.SignedTensor.continuous_rep line 1960
  178. lemma OAI.SpinAngle.SignedCarrier.continuous_rep line 1967
  179. lemma OAI.SpinAngle.TensorRep.tensor_posSemidef line 1976
  180. lemma OAI.SpinAngle.TensorRep.action_positive line 1989
  181. lemma OAI.SpinAngle.PolynomialCarrier.hermitianAction_positive line 1999
  182. def OAI.SpinAngle.PolynomialCarrier.highestVector line 2006
  183. lemma OAI.SpinAngle.PolynomialCarrier.highestVector_ne_zero line 2009
  184. lemma OAI.SpinAngle.PolynomialCarrier.inclusion_linear_hermitianAction line 2014
  185. lemma OAI.SpinAngle.PolynomialCarrier.highestVector_diagonal line 2020
  186. lemma OAI.SpinAngle.PolynomialCarrier.card_rowColor line 2035
  187. lemma OAI.SpinAngle.PolynomialCarrier.highestMonomial_eq_rowLen line 2043
  188. lemma OAI.SpinAngle.PolynomialCarrier.sum_rowLen_eq_card line 2050
  189. lemma OAI.SpinAngle.TensorPositive.mapL_nonneg line 2067
  190. lemma OAI.SpinAngle.TensorPositive.map_positive line 2085
  191. lemma OAI.SpinAngle.TensorPositive.map_norm_bound line 2095
  192. def OAI.SpinAngle.EntropyMonomial.entropy line 2119

    Also declared: ComparatorChallenges/SpinAngle.lean:337 (same declaration text).

  193. lemma OAI.SpinAngle.EntropyMonomial.sum_log_ratio line 2122
  194. lemma OAI.SpinAngle.EntropyMonomial.power_le_exponential line 2136
  195. theorem OAI.SpinAngle.EntropyMonomial.prod_pow_le line 2162
  196. lemma OAI.SpinAngle.EntropyMonomial.optimal_prod line 2189
  197. lemma OAI.SpinAngle.PositiveTrace.eigenvalues_nonneg line 2209
  198. theorem OAI.SpinAngle.PositiveTrace.eigenvalue_le_trace line 2217
  199. def OAI.SpinAngle.Isotypic.space line 2253

    Also declared: ComparatorChallenges/SpinAngle.lean:349 (same declaration text).

  200. def OAI.SpinAngle.Isotypic.projection line 2267

    Also declared: ComparatorChallenges/SpinAngle.lean:363 (same declaration text).

  201. lemma OAI.SpinAngle.Isotypic.projection_mem line 2269
  202. lemma OAI.SpinAngle.Isotypic.projection_norm_apply_le line 2282
  203. lemma OAI.SpinAngle.Isotypic.map_mem line 2295
  204. lemma OAI.SpinAngle.Isotypic.endomorphism_mem line 2308
  205. lemma OAI.SpinAngle.Isotypic.natural_mem line 2318
  206. lemma OAI.SpinAngle.Isotypic.scalar_on_space line 2330
  207. lemma OAI.SpinAngle.Isotypic.exists_nonzero_adjoint line 2349
  208. lemma OAI.SpinAngle.Isotypic.transfer_eigenvalue_bound line 2364
  209. theorem OAI.SpinAngle.Isotypic.norm_bound line 2383
  210. lemma OAI.SpinAngle.Isotypic.projection_commute_of_invariant line 2410
  211. lemma OAI.SpinAngle.Isotypic.projection_commute_endomorphism line 2425
  212. lemma OAI.SpinAngle.Isotypic.projection_commute_natural line 2430
  213. def OAI.SpinAngle.SignedTensor.IsEvenDensity line 2442
  214. lemma OAI.SpinAngle.SignedTensor.block_posSemidef line 2445
  215. lemma OAI.SpinAngle.SignedCarrier.hermitianAction_positive line 2467
  216. lemma OAI.SpinAngle.SignedCarrier.hermitianAction_norm_bound line 2475
  217. def OAI.SpinAngle.SignedCarrier.parts line 2487

    Also declared: ComparatorChallenges/SpinAngle.lean:390 (same declaration text).

  218. def OAI.SpinAngle.SignedCarrier.entropy line 2488

    Also declared: ComparatorChallenges/SpinAngle.lean:391 (same declaration text).

  219. def OAI.SpinAngle.SignedCarrier.dimension line 2489

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:392 (same statement text; different proof or body). Qualify references as OAI.SpinAngle.SignedCarrier.dimension@path.

  220. lemma OAI.SpinAngle.SignedCarrier.sum_parts line 2492
  221. lemma OAI.SpinAngle.SignedCarrier.entropy_eq_source line 2498
  222. lemma OAI.SpinAngle.SignedCarrier.hermitianAction_density_bound line 2508
  223. lemma OAI.SpinAngle.EntropyMonomial.exists_optimal line 2539
  224. abbrev OAI.SpinAngle.SignedCarrier.typeProjection line 2567

    Also declared: ComparatorChallenges/SpinAngle.lean:396 (same declaration text).

  225. lemma OAI.SpinAngle.SignedCarrier.density_on_space line 2570
  226. lemma OAI.SpinAngle.SignedCarrier.projected_density_bound line 2584
  227. theorem OAI.SpinAngle.SignedCarrier.global_density_upper line 2595
  228. def OAI.SpinAngle.SignedCarrier.highestVector line 2602
  229. lemma OAI.SpinAngle.SignedCarrier.highestVector_ne_zero line 2605
  230. lemma OAI.SpinAngle.SignedCarrier.highestVector_diagonal line 2613
  231. lemma OAI.SpinAngle.SignedCarrier.exists_density_trace_lower line 2629
  232. abbrev OAI.SpinAngle.DenseLU.Mat line 2655
  233. def OAI.SpinAngle.DenseLU.border line 2657
  234. lemma OAI.SpinAngle.DenseLU.border_zero_zero line 2660
  235. lemma OAI.SpinAngle.DenseLU.border_zero_succ line 2662
  236. lemma OAI.SpinAngle.DenseLU.border_succ_zero line 2664
  237. lemma OAI.SpinAngle.DenseLU.border_succ_succ line 2666
  238. lemma OAI.SpinAngle.DenseLU.border_eq line 2669
  239. lemma OAI.SpinAngle.DenseLU.continuous_border line 2675
  240. lemma OAI.SpinAngle.DenseLU.border_factor line 2690
  241. def OAI.SpinAngle.DenseLU.LowerUnipotent line 2700
  242. lemma OAI.SpinAngle.DenseLU.lower_border line 2703
  243. lemma OAI.SpinAngle.DenseLU.upper_border line 2718
  244. def OAI.SpinAngle.DenseLU.bigCell line 2727
  245. lemma OAI.SpinAngle.DenseLU.border_mem_bigCell line 2730
  246. theorem OAI.SpinAngle.DenseLU.dense_bigCell line 2739
  247. lemma OAI.SpinAngle.PolynomialCarrier.action_mem_alternating line 2776
  248. lemma OAI.SpinAngle.PolynomialCarrier.upper_weight_support line 2782
  249. lemma OAI.SpinAngle.PolynomialCarrier.upper_highest line 2801
  250. lemma OAI.SpinAngle.PolynomialCarrier.continuous_action_highest line 2817
  251. lemma OAI.SpinAngle.PolynomialCarrier.action_highest_mem_of_lower line 2826
  252. def OAI.SpinAngle.PolyDimension.boundedExponentEquiv line 2850
  253. theorem OAI.SpinAngle.PolyDimension.finrank_restrictDegree line 2858
  254. abbrev OAI.SpinAngle.PolyDimension.LowerIndex line 2868
  255. lemma OAI.SpinAngle.PolyDimension.card_lowerIndex line 2870
  256. lemma OAI.SpinAngle.PolyDimension.twice_card_lowerIndex line 2874
  257. def OAI.SpinAngle.PolyDimension.lowerEntry line 2879
  258. lemma OAI.SpinAngle.PolyDimension.lowerEntry_degree line 2882
  259. lemma OAI.SpinAngle.PolyDimension.totalDegree_sum_le line 2886
  260. def OAI.SpinAngle.PolyDimension.valueTranspose line 2903
  261. lemma OAI.SpinAngle.PolyDimension.value_mem_range line 2909
  262. lemma OAI.SpinAngle.PolyDimension.finrank_value_range line 2920
  263. def OAI.SpinAngle.PolynomialCarrier.lowerCoordinate line 2939
  264. lemma OAI.SpinAngle.PolynomialCarrier.lowerCoordinate_degree line 2942
  265. def OAI.SpinAngle.PolynomialCarrier.lowerCoordinateBounded line 2951
  266. def OAI.SpinAngle.PolynomialCarrier.lowerParameters line 2957
  267. lemma OAI.SpinAngle.PolynomialCarrier.eval_lowerEntry line 2960
  268. lemma OAI.SpinAngle.PolynomialCarrier.eval_lowerCoordinate line 2969
  269. theorem OAI.SpinAngle.PolynomialCarrier.ordinary_finrank_le line 2983
  270. def OAI.SpinAngle.CompactTwirl.compactHaar line 3033
  271. instance OAI.SpinAngle.CompactTwirl.(instance at line 3036) line 3036
  272. instance OAI.SpinAngle.CompactTwirl.(instance at line 3039) line 3039
  273. lemma OAI.SpinAngle.CompactTwirl.continuous_integrable line 3042
  274. def OAI.SpinAngle.CompactTwirl.conjugate line 3049
  275. def OAI.SpinAngle.CompactTwirl.twirl line 3051
  276. lemma OAI.SpinAngle.CompactTwirl.continuous_conjugate line 3053
  277. lemma OAI.SpinAngle.CompactTwirl.integrable_conjugate line 3068
  278. lemma OAI.SpinAngle.CompactTwirl.conjugate_mul line 3072
  279. lemma OAI.SpinAngle.CompactTwirl.twirl_commute line 3088
  280. lemma OAI.SpinAngle.CompactTwirl.twirl_trace line 3100
  281. lemma OAI.SpinAngle.CompactTwirl.twirl_nonneg line 3111
  282. lemma OAI.SpinAngle.unitaryGroup_compactSpace line 3143
  283. def OAI.SpinAngle.CompactTwirl.continuousAction line 3160
  284. lemma OAI.SpinAngle.CompactTwirl.continuousAction_apply line 3163
  285. def OAI.SpinAngle.CompactTwirl.operatorTrace line 3177
  286. lemma OAI.SpinAngle.CompactTwirl.operatorTrace_apply line 3181
  287. lemma OAI.SpinAngle.CompactTwirl.operatorTrace_mul_comm line 3195
  288. theorem OAI.SpinAngle.CompactTwirl.twirl_irreducible line 3212
  289. lemma OAI.SpinAngle.CompactTwirl.twirl_natural line 3251
  290. lemma OAI.SpinAngle.CompactTwirl.continuousAction_inverse_star line 3266
  291. lemma OAI.SpinAngle.ProjectionOrder.scalar_projection_le line 3293
  292. lemma OAI.SpinAngle.CompactTwirl.isotypic_twirl_scalar line 3315
  293. lemma OAI.SpinAngle.CompactTwirl.isotypic_twirl_lower line 3333
  294. lemma OAI.SpinAngle.CompactMixture.convexHull_compact line 3368
  295. lemma OAI.SpinAngle.CompactTwirl.twirl_finite_mixture line 3424
  296. lemma OAI.SpinAngle.SignedCarrier.dimension_eq line 3451
  297. lemma OAI.SpinAngle.SignedCarrier.dimension_pos line 3456
  298. theorem OAI.SpinAngle.SignedCarrier.dimension_le line 3462
  299. def OAI.SpinAngle.SignedTensor.conjugateDensity line 3484
  300. lemma OAI.SpinAngle.SignedTensor.conjugateDensity_isEvenDensity line 3487
  301. lemma OAI.SpinAngle.SignedTensor.block_conjugateDensity line 3497
  302. lemma OAI.SpinAngle.SignedTensor.tensor_conjugateDensity line 3504
  303. instance OAI.SpinAngle.SignedTensor.groupMeasurableSpace line 3520
  304. instance OAI.SpinAngle.SignedTensor.groupBorelSpace line 3521
  305. instance OAI.SpinAngle.SignedTensor.groupCompactSpace line 3523
  306. lemma OAI.SpinAngle.SignedCarrier.projection_isStarProjection line 3534
  307. lemma OAI.SpinAngle.SignedCarrier.twirl_lower line 3538
  308. lemma OAI.SpinAngle.ProjectionOrder.rescale_trace_lower line 3560
  309. lemma OAI.SpinAngle.MatrixBridge.inverse_mono line 3575
  310. theorem OAI.SpinAngle.SignedCarrier.exists_density_mixture line 3590
  311. lemma OAI.SpinAngle.MatrixBridge.inverse_real_smul line 3615
  312. lemma OAI.SpinAngle.MatrixBridge.forward_real_smul line 3620
  313. lemma OAI.SpinAngle.MatrixBridge.forward_norm line 3625
  314. lemma OAI.SpinAngle.MatrixBridge.inverse_norm line 3627
  315. lemma OAI.SpinAngle.MatrixBridge.inverse_toContinuous line 3631
  316. def OAI.SpinAngle.SignedCarrier.matrixProjection line 3643

    Also declared: ComparatorChallenges/SpinAngle.lean:399 (same declaration text).

  317. lemma OAI.SpinAngle.SignedCarrier.matrixProjection_isStarProjection line 3646
  318. lemma OAI.SpinAngle.SignedCarrier.inverse_action line 3658
  319. lemma OAI.SpinAngle.SignedCarrier.matrix_density_upper line 3663
  320. lemma OAI.SpinAngle.SignedCarrier.density_projection_commute line 3670
  321. lemma OAI.SpinAngle.SignedCarrier.matrix_density_commute line 3684
  322. theorem OAI.SpinAngle.SignedCarrier.exists_matrix_density_mixture line 3693
  323. lemma OAI.SpinAngle.SignedTensor.block_add line 3709
  324. lemma OAI.SpinAngle.SignedTensor.block_real_smul line 3714
  325. lemma OAI.SpinAngle.SignedTensor.block_zero line 3719
  326. lemma OAI.SpinAngle.SignedTensor.block_sum line 3724
  327. lemma OAI.SpinAngle.SignedTensor.block_trace line 3731
  328. def OAI.SpinAngle.SignedTensor.evenAverage line 3738
  329. lemma OAI.SpinAngle.SignedTensor.evenAverage_isEvenDensity line 3741
  330. abbrev OAI.SpinAngle.MatrixAnalysis.Mat line 3771

    Also declared: ComparatorChallenges/SpinAngle.lean:458 (same declaration text).

  331. def OAI.SpinAngle.MatrixAnalysis.root line 3774
  332. def OAI.SpinAngle.MatrixAnalysis.invRoot line 3776
  333. def OAI.SpinAngle.MatrixAnalysis.support line 3778
  334. lemma OAI.SpinAngle.MatrixAnalysis.root_selfAdjoint line 3780
  335. lemma OAI.SpinAngle.MatrixAnalysis.root_nonneg line 3782
  336. lemma OAI.SpinAngle.MatrixAnalysis.invRoot_selfAdjoint line 3784
  337. lemma OAI.SpinAngle.MatrixAnalysis.invRoot_nonneg line 3786
  338. lemma OAI.SpinAngle.MatrixAnalysis.support_selfAdjoint line 3788
  339. lemma OAI.SpinAngle.MatrixAnalysis.root_mul_self line 3791
  340. lemma OAI.SpinAngle.MatrixAnalysis.invRoot_mul_root line 3801
  341. lemma OAI.SpinAngle.MatrixAnalysis.support_isStarProjection line 3813
  342. lemma OAI.SpinAngle.MatrixAnalysis.mul_support line 3823
  343. lemma OAI.SpinAngle.MatrixAnalysis.root_mul_support line 3834
  344. lemma OAI.SpinAngle.MatrixAnalysis.root_commute line 3841
  345. lemma OAI.SpinAngle.MatrixAnalysis.invRoot_commute line 3843
  346. lemma OAI.SpinAngle.MatrixAnalysis.support_commute line 3845
  347. lemma OAI.SpinAngle.MatrixAnalysis.norm_le_re_trace line 3850
  348. lemma OAI.SpinAngle.MatrixAnalysis.norm_sq_le_re_trace_star_mul_self line 3864
  349. lemma OAI.SpinAngle.MatrixAnalysis.root_mul_support_of_le_smul line 3871
  350. lemma OAI.SpinAngle.MatrixAnalysis.invRoot_mul_self_mul_invRoot line 3894
  351. lemma OAI.SpinAngle.MatrixAnalysis.cell_trace_identity line 3905
  352. lemma OAI.SpinAngle.MatrixAnalysis.cell_trace_nonneg line 3920
  353. lemma OAI.SpinAngle.MatrixAnalysis.re_trace_nonneg line 3926
  354. lemma OAI.SpinAngle.MatrixAnalysis.re_trace_mono line 3932
  355. lemma OAI.SpinAngle.MatrixAnalysis.re_trace_projection_mul_le line 3938
  356. lemma OAI.SpinAngle.MatrixAnalysis.cell_norm_sq_le_trace line 3947
  357. def OAI.SpinAngle.TensorMatrix.tensor line 3961
  358. lemma OAI.SpinAngle.TensorMatrix.tensor_star line 3963
  359. lemma OAI.SpinAngle.TensorMatrix.tensor_mul line 3973
  360. lemma OAI.SpinAngle.TensorMatrix.tensor_one line 3986
  361. lemma OAI.SpinAngle.TensorMatrix.tensor_trace line 4003
  362. lemma OAI.SpinAngle.TensorMatrix.tensor_nonneg line 4014
  363. lemma OAI.SpinAngle.TensorMatrix.tensor_selfAdjoint line 4024
  364. lemma OAI.SpinAngle.TensorMatrix.tensor_norm_sq_le_trace_product line 4032
  365. lemma OAI.SpinAngle.TensorMatrix.tensor_norm_sq_le_re_trace_product line 4038
  366. lemma OAI.SpinAngle.TensorMatrix.tensor_cell_norm_sq_le_product line 4049
  367. def OAI.SpinAngle.missingCellFactor line 4065

    Also declared: ComparatorChallenges/SpinAngle.lean:406 (same declaration text).

  368. def OAI.SpinAngle.missingCellProductFactor line 4068

    Distinct definitions of this name: ComparatorChallenges/SpinAngle.lean:409 (same statement text; different proof or body). Qualify references as OAI.SpinAngle.missingCellProductFactor@path.

  369. lemma OAI.SpinAngle.missingCellFactor_nonneg line 4071
  370. lemma OAI.SpinAngle.missingCellFactor_le_exp line 4075
  371. theorem OAI.SpinAngle.missingCellProduct line 4094
  372. lemma OAI.SpinAngle.retained_product_le line 4111
  373. def OAI.SpinAngle.occupiedRow line 4150

    Also declared: ComparatorChallenges/SpinAngle.lean:414 (same declaration text).

  374. def OAI.SpinAngle.missingInRow line 4153

    Also declared: ComparatorChallenges/SpinAngle.lean:417 (same declaration text).

  375. lemma OAI.SpinAngle.occupiedRow_card_le line 4156
  376. lemma OAI.SpinAngle.missingInRow_le line 4164
  377. lemma OAI.SpinAngle.retained_factor_eq_missingCellFactor line 4172
  378. lemma OAI.SpinAngle.prod_occupiedRow line 4183
  379. lemma OAI.SpinAngle.board_product_le line 4201
  380. structure OAI.SpinAngle.MatrixAnalysis.Density line 4220
  381. instance OAI.SpinAngle.MatrixAnalysis.(instance at line 4225) line 4225
  382. def OAI.SpinAngle.MatrixAnalysis.average line 4227
  383. lemma OAI.SpinAngle.MatrixAnalysis.average_nonneg line 4230
  384. lemma OAI.SpinAngle.MatrixAnalysis.sum_eq_smul_average line 4238
  385. lemma OAI.SpinAngle.MatrixAnalysis.le_smul_average line 4248
  386. lemma OAI.SpinAngle.MatrixAnalysis.support_cell_trace_sum line 4253
  387. theorem OAI.SpinAngle.normalized_board_bound line 4278
  388. abbrev OAI.SpinAngle.DependentTensor.Mat line 4309

    Also declared: ComparatorChallenges/SpinAngle.lean:426 (same declaration text).

  389. def OAI.SpinAngle.DependentTensor.tensor line 4311

    Also declared: ComparatorChallenges/SpinAngle.lean:428 (same declaration text).

  390. lemma OAI.SpinAngle.DependentTensor.tensor_star line 4313
  391. lemma OAI.SpinAngle.DependentTensor.tensor_mul line 4323
  392. lemma OAI.SpinAngle.DependentTensor.tensor_one line 4334
  393. lemma OAI.SpinAngle.DependentTensor.tensor_nonneg line 4350
  394. lemma OAI.SpinAngle.DependentTensor.tensor_projection line 4360
  395. lemma OAI.SpinAngle.DependentTensor.tensor_sum line 4374
  396. lemma OAI.SpinAngle.DependentTensor.tensor_smul line 4387
  397. lemma OAI.SpinAngle.DependentTensor.tensor_sum_smul line 4401
  398. lemma OAI.SpinAngle.DependentTensor.tensor_mono line 4408
  399. abbrev OAI.SpinAngle.BlockTensor.Fiber line 4430

    Also declared: ComparatorChallenges/SpinAngle.lean:438 (same declaration text).

  400. def OAI.SpinAngle.BlockTensor.splitEquiv line 4432

    Also declared: ComparatorChallenges/SpinAngle.lean:440 (same declaration text).

  401. def OAI.SpinAngle.BlockTensor.tensor line 4443

    Also declared: ComparatorChallenges/SpinAngle.lean:450 (same declaration text).

  402. lemma OAI.SpinAngle.BlockTensor.tensor_mul line 4446
  403. lemma OAI.SpinAngle.BlockTensor.tensor_star line 4452
  404. lemma OAI.SpinAngle.BlockTensor.tensor_one line 4465
  405. lemma OAI.SpinAngle.BlockTensor.tensor_nonneg line 4471
  406. lemma OAI.SpinAngle.BlockTensor.tensor_mono line 4474
  407. lemma OAI.SpinAngle.BlockTensor.tensor_projection line 4480
  408. lemma OAI.SpinAngle.BlockTensor.tensor_sum_smul line 4494
  409. lemma OAI.SpinAngle.BlockTensor.prod_fibers line 4510
  410. lemma OAI.SpinAngle.BlockTensor.tensor_cells line 4524
  411. lemma OAI.SpinAngle.BlockTensor.tensor_commute line 4539
  412. lemma OAI.SpinAngle.TensorMatrix.tensor_root_square line 4554
  413. lemma OAI.SpinAngle.TensorMatrix.tensor_root line 4561
  414. lemma OAI.SpinAngle.TensorMatrix.tensor_invRoot_mul_root line 4567
  415. lemma OAI.SpinAngle.TensorMatrix.tensor_root_mul_support_of_le_smul line 4575
  416. lemma OAI.SpinAngle.sum_occupiedRow_card line 4590
  417. lemma OAI.SpinAngle.sum_missingInRow line 4601
  418. lemma OAI.SpinAngle.boardPhi_nonneg line 4610
  419. lemma OAI.SpinAngle.boardPhi_le_exp_holes line 4614
  420. structure OAI.SpinAngle.TypeLabel line 4631

    Also declared: ComparatorChallenges/SpinAngle.lean:466 (same declaration text).

  421. def OAI.SpinAngle.TypeLabel.size line 4639

    Also declared: ComparatorChallenges/SpinAngle.lean:474 (same declaration text).

  422. def OAI.SpinAngle.TypeLabel.entropy line 4640

    Also declared: ComparatorChallenges/SpinAngle.lean:475 (same declaration text).

  423. def OAI.SpinAngle.TypeLabel.dimension line 4641

    Also declared: ComparatorChallenges/SpinAngle.lean:476 (same declaration text).

  424. def OAI.SpinAngle.TypeLabel.projection line 4643

    Also declared: ComparatorChallenges/SpinAngle.lean:478 (same declaration text).

  425. lemma OAI.SpinAngle.TypeLabel.projection_isStarProjection line 4647
  426. lemma OAI.SpinAngle.TypeLabel.dimension_pos line 4651
  427. lemma OAI.SpinAngle.TypeLabel.dimension_le line 4654
  428. lemma OAI.SpinAngle.TypeLabel.entropy_eq_zero_of_size_zero line 4657
  429. abbrev OAI.SpinAngle.EvenDensity line 4669
  430. def OAI.SpinAngle.EvenDensity.matrix line 4672
  431. lemma OAI.SpinAngle.EvenDensity.nonneg line 4674
  432. lemma OAI.SpinAngle.EvenDensity.trace_eq_one line 4676
  433. def OAI.SpinAngle.EvenDensity.toDensity line 4680
  434. def OAI.SpinAngle.EvenDensity.mean line 4684
  435. lemma OAI.SpinAngle.EvenDensity.mean_matrix line 4687
  436. lemma OAI.SpinAngle.TypeLabel.density_upper line 4697
  437. lemma OAI.SpinAngle.TypeLabel.density_commute line 4701
  438. lemma OAI.SpinAngle.TypeLabel.density_mixture line 4706
  439. abbrev OAI.SpinAngle.TypeBlocks.Fiber line 4723

    Also declared: ComparatorChallenges/SpinAngle.lean:490 (same declaration text).

  440. def OAI.SpinAngle.TypeBlocks.projection line 4725

    Also declared: ComparatorChallenges/SpinAngle.lean:492 (same declaration text).

  441. def OAI.SpinAngle.TypeBlocks.entropy line 4728

    Also declared: ComparatorChallenges/SpinAngle.lean:495 (same declaration text).

  442. def OAI.SpinAngle.TypeBlocks.dimension line 4729

    Also declared: ComparatorChallenges/SpinAngle.lean:496 (same declaration text).

  443. lemma OAI.SpinAngle.TypeBlocks.projection_isStarProjection line 4731
  444. lemma OAI.SpinAngle.TypeBlocks.density_commute line 4735
  445. theorem OAI.SpinAngle.TypeBlocks.density_mixture line 4751