OAI/Analysis/Naimark/Representations.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NaimarkZFC.irreducible_commutant_scalar line 13
  2. theorem OAI.NaimarkZFC.inner_realPart_operator line 35
  3. def OAI.NaimarkZFC.diagonalOperator line 47
  4. theorem OAI.NaimarkZFC.diagonalOperator_apply line 54
  5. def OAI.NaimarkZFC.diagonalHom line 57
  6. def OAI.NaimarkZFC.diagonalRepresentation line 76
  7. def OAI.NaimarkZFC.coordinateInclusion line 80
  8. theorem OAI.NaimarkZFC.coordinateInclusion_apply line 86
  9. theorem OAI.NaimarkZFC.sum_coordinateInclusion line 91
  10. theorem OAI.NaimarkZFC.diagonalOperator_coordinateInclusion line 97
  11. def OAI.NaimarkZFC.amplificationBlock line 104
  12. theorem OAI.NaimarkZFC.amplificationBlock_apply line 110
  13. theorem OAI.NaimarkZFC.amplificationBlock_sum line 115
  14. theorem OAI.NaimarkZFC.amplified_commutant_commute line 123
  15. theorem OAI.NaimarkZFC.irreducible_finite_strong_density line 147
  16. theorem OAI.NaimarkZFC.irreducible_selfAdjoint_strong_density line 185
  17. def OAI.NaimarkZFC.saResolvent line 246
  18. theorem OAI.NaimarkZFC.sa_spectrum_sub_ne_zero line 248
  19. theorem OAI.NaimarkZFC.saResolvent_continuousOn line 254
  20. theorem OAI.NaimarkZFC.saResolvent_inverse line 259
  21. theorem OAI.NaimarkZFC.saResolvent_norm_le line 273
  22. theorem OAI.NaimarkZFC.saResolvent_star line 283
  23. def OAI.NaimarkZFC.saBoundedTransform line 293
  24. theorem OAI.NaimarkZFC.saBoundedTransform_selfAdjoint line 295
  25. theorem OAI.NaimarkZFC.saBoundedTransform_norm_le line 301
  26. theorem OAI.NaimarkZFC.resolvent_sum_real line 308
  27. theorem OAI.NaimarkZFC.saBoundedTransform_eq_cfc line 317
  28. def OAI.NaimarkZFC.rationalPreimage line 328
  29. theorem OAI.NaimarkZFC.rationalPreimage_continuous line 330
  30. theorem OAI.NaimarkZFC.rationalPreimage_rightInverse line 336
  31. theorem OAI.NaimarkZFC.saBoundedTransform_preimage line 347
  32. theorem OAI.NaimarkZFC.saResolvent_sub line 370
  33. theorem OAI.NaimarkZFC.map_saBoundedTransform line 384
  34. theorem OAI.NaimarkZFC.saResolvent_eval_sub_le line 393
  35. def OAI.NaimarkZFC.irreducibleUnitalRepresentation line 408
  36. theorem OAI.NaimarkZFC.irreducibleUnitalRepresentation_apply line 420
  37. theorem OAI.NaimarkZFC.irreducible_bounded_strong_density line 424
  38. theorem OAI.NaimarkZFC.irreducible_bounded_strong_density_scaled line 462
  39. def OAI.NaimarkZFC.symmetricCompression line 500
  40. theorem OAI.NaimarkZFC.symmetricCompression_selfAdjoint line 502
  41. theorem OAI.NaimarkZFC.symmetricCompression_mul_projection line 510
  42. theorem OAI.NaimarkZFC.symmetricCompression_norm_le line 516
  43. theorem OAI.NaimarkZFC.norm_mul_starProjection_le_sum line 535
  44. theorem OAI.NaimarkZFC.symmetricCompression_apply_of_mem line 550
  45. theorem OAI.NaimarkZFC.irreducible_selfAdjoint_correction line 561
  46. theorem OAI.NaimarkZFC.irreducible_selfAdjoint_transitivity line 610
  47. theorem OAI.NaimarkZFC.exists_selfAdjoint_operator_vector line 688
  48. theorem OAI.NaimarkZFC.irreducible_selfAdjoint_vector line 710
  49. def OAI.NaimarkZFC.saCayley line 719
  50. theorem OAI.NaimarkZFC.saCayley_eq line 722
  51. theorem OAI.NaimarkZFC.saCayley_unitary line 730
  52. theorem OAI.NaimarkZFC.irreducible_unitary_vector line 744
  53. theorem OAI.NaimarkZFC.UnitarilyEquivalent.refl line 787
  54. theorem OAI.NaimarkZFC.UnitarilyEquivalent.symm line 790
  55. theorem OAI.NaimarkZFC.UnitarilyEquivalent.trans line 798
  56. theorem OAI.NaimarkZFC.cyclic_representation_equivalent line 809
  57. theorem OAI.NaimarkZFC.irreducible_equivalent_of_coefficients line 816
  58. theorem OAI.NaimarkZFC.equivalent_vector_states_unitary line 834
  59. theorem OAI.NaimarkZFC.irreducible_adjoint_transitivity line 858
  60. theorem OAI.NaimarkZFC.irreducible_null_decomposition line 888
  61. def OAI.NaimarkZFC.vectorNullAlgebra line 911
  62. instance OAI.NaimarkZFC.vectorNullAlgebra_closed line 928
  63. instance OAI.NaimarkZFC.(instance at line 935) line 935
  64. instance OAI.NaimarkZFC.(instance at line 938) line 938
  65. theorem OAI.NaimarkZFC.star_mul_self_mem_vectorNullAlgebra line 941
  66. lemma OAI.NaimarkZFC.vectorNullAlgebra_coe_nonneg line 947
  67. theorem OAI.NaimarkZFC.vectorNull_approximateUnit_annihilates line 958
  68. theorem OAI.NaimarkZFC.vectorNull_complement_properties line 1001
  69. theorem OAI.NaimarkZFC.irreducible_vector_excision line 1015
  70. theorem OAI.NaimarkZFC.pure_state_excision line 1053
  71. theorem OAI.NaimarkZFC.approximateUnit_strong line 1083
  72. theorem OAI.NaimarkZFC.nullAlgebra_vector_coefficient line 1142
  73. theorem OAI.NaimarkZFC.inequivalent_nullAlgebra_common_kernel line 1172
  74. theorem OAI.NaimarkZFC.inequivalent_nullAlgebra_complement_strong line 1190
  75. lemma OAI.NaimarkZFC.positive_contraction_square_le line 1208
  76. theorem OAI.NaimarkZFC.cross_excision_bound line 1215
  77. theorem OAI.NaimarkZFC.cross_excision_tendsto line 1246
  78. def OAI.NaimarkZFC.ExcisionIndex line 1283
  79. instance OAI.NaimarkZFC.ExcisionIndex.(instance at line 1288) line 1288
  80. instance OAI.NaimarkZFC.ExcisionIndex.(instance at line 1289) line 1289
  81. instance OAI.NaimarkZFC.ExcisionIndex.(instance at line 1290) line 1290
  82. theorem OAI.NaimarkZFC.ExcisionIndex.tendsto_coe line 1296
  83. lemma OAI.NaimarkZFC.vectorNullAlgebra_coe_le line 1311
  84. def OAI.NaimarkZFC.pureExcisionNet line 1320
  85. lemma OAI.NaimarkZFC.pureExcisionNet_nonneg line 1323
  86. lemma OAI.NaimarkZFC.pureExcisionNet_norm line 1328
  87. lemma OAI.NaimarkZFC.pureExcisionNet_antitone line 1333
  88. lemma OAI.NaimarkZFC.pureExcisionNet_fixes line 1339
  89. lemma OAI.NaimarkZFC.pureExcisionNet_excision line 1344
  90. lemma OAI.NaimarkZFC.pureExcisionNet_inequivalent_strong line 1350
  91. theorem OAI.NaimarkZFC.pureExcisionNet_cross line 1359
  92. theorem OAI.NaimarkZFC.strong_zero_of_nondegenerate line 1384
  93. theorem OAI.NaimarkZFC.excision_null_mul_tendsto line 1425
  94. theorem OAI.NaimarkZFC.excision_inequivalent_strong line 1444
  95. theorem OAI.NaimarkZFC.irreducible_nullAlgebra_fixes_orthogonal line 1466
  96. theorem OAI.NaimarkZFC.excision_orthogonal_strong line 1486
  97. theorem OAI.NaimarkZFC.positiveTrace_sandwich line 1502
  98. theorem OAI.NaimarkZFC.positive_dini line 1538
  99. abbrev OAI.NaimarkZFC.SequenceDiagonal line 1560
  100. def OAI.NaimarkZFC.peakingCoefficientsFun line 1564
  101. theorem OAI.NaimarkZFC.peakingCoefficientsFun_nat line 1568
  102. theorem OAI.NaimarkZFC.peakingCoefficientsFun_infty line 1571
  103. theorem OAI.NaimarkZFC.peakingCoefficientsFun_norm_le line 1574
  104. def OAI.NaimarkZFC.peakingCoefficients line 1584
  105. theorem OAI.NaimarkZFC.peakingCoefficients_nat line 1601
  106. theorem OAI.NaimarkZFC.peakingCoefficients_infty line 1604
  107. def OAI.NaimarkZFC.peakingCoefficientsPositive line 1607
  108. theorem OAI.NaimarkZFC.trace_sandwich_tendsto line 1617
  109. theorem OAI.NaimarkZFC.peaking_endpoint_decay line 1627
  110. lemma OAI.NaimarkZFC.state_norm_sq_le line 1673
  111. lemma OAI.NaimarkZFC.trace_excision_square_bound line 1691
  112. theorem OAI.NaimarkZFC.excision_trace_null_of_small_projections line 1716
  113. lemma OAI.NaimarkZFC.projection_exists_unit_fixed line 1742
  114. lemma OAI.NaimarkZFC.irreducible_small_projection_value_one line 1754
  115. theorem OAI.NaimarkZFC.pureExcisionNet_trace_null line 1772
  116. theorem OAI.NaimarkZFC.vector_sandwich_tendsto line 1794
  117. def OAI.NaimarkZFC.pureGNS line 1805
  118. theorem OAI.NaimarkZFC.peaking_endpoint_of_excision line 1808