OAI/Analysis/Naimark/Stages.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.NaimarkZFC.TracialStage line 12
  2. instance OAI.NaimarkZFC.(instance at line 26) line 26
  3. theorem OAI.NaimarkZFC.TracialStage.traceFaithful line 32
  4. lemma OAI.NaimarkZFC.TracialStage.infinite line 35
  5. def OAI.NaimarkZFC.TracialStage.reference line 39
  6. lemma OAI.NaimarkZFC.TracialStage.reference_spec line 42
  7. lemma OAI.NaimarkZFC.TracialStage.reference_peaks line 46
  8. structure OAI.NaimarkZFC.TracialStage.Hom line 50
  9. def OAI.NaimarkZFC.TracialStage.Hom.id line 60
  10. def OAI.NaimarkZFC.TracialStage.Hom.comp line 67
  11. lemma OAI.NaimarkZFC.TracialStage.Hom.comp_map line 74
  12. lemma OAI.NaimarkZFC.TracialStage.Hom.id_map line 75
  13. lemma OAI.NaimarkZFC.TracialStage.Hom.reference_map line 77
  14. instance OAI.NaimarkZFC.TracialStage.(instance at line 89) line 89
  15. def OAI.NaimarkZFC.TracialStage.initial line 97
  16. def OAI.NaimarkZFC.TracialStage.positiveTrace line 116
  17. lemma OAI.NaimarkZFC.TracialStage.positiveTrace_normalized line 118
  18. lemma OAI.NaimarkZFC.TracialStage.positiveTrace_faithful line 119
  19. def OAI.NaimarkZFC.TracialStage.hnn line 129
  20. def OAI.NaimarkZFC.TracialStage.hnnHom line 142
  21. lemma OAI.NaimarkZFC.TracialStage.hnn_reference line 150
  22. theorem OAI.NaimarkZFC.TracialStage.hnn_reference_join line 157
  23. def OAI.NaimarkZFC.KOS.projectionCutoff line 173
  24. lemma OAI.NaimarkZFC.KOS.projectionCutoff_den_pos line 175
  25. lemma OAI.NaimarkZFC.KOS.continuous_projectionCutoff line 178
  26. lemma OAI.NaimarkZFC.KOS.projectionCutoff_nonneg line 183
  27. lemma OAI.NaimarkZFC.KOS.projectionCutoff_le_one line 186
  28. lemma OAI.NaimarkZFC.KOS.projectionCutoff_zero line 191
  29. lemma OAI.NaimarkZFC.KOS.projectionCutoff_one line 192
  30. def OAI.NaimarkZFC.KOS.projectionTruncate line 196
  31. lemma OAI.NaimarkZFC.KOS.projectionTruncate_nonneg line 198
  32. lemma OAI.NaimarkZFC.KOS.projectionTruncate_le_one line 201
  33. lemma OAI.NaimarkZFC.KOS.projectionTruncate_relation line 205
  34. lemma OAI.NaimarkZFC.KOS.projectionTruncate_apply line 219
  35. theorem OAI.NaimarkZFC.KOS.exact_gram_projection line 233
  36. theorem OAI.NaimarkZFC.KOS.difference_span_coefficients line 268
  37. theorem OAI.NaimarkZFC.KOS.difference_projection_bound line 284
  38. theorem OAI.NaimarkZFC.KOS.gram_combination_error line 323
  39. theorem OAI.NaimarkZFC.KOS.gram_zero_combination_bound line 358
  40. theorem OAI.NaimarkZFC.KOS.finite_orthonormal_coordinates line 373
  41. theorem OAI.NaimarkZFC.KOS.gram_cross_zero line 397
  42. theorem OAI.NaimarkZFC.KOS.gram_sum_projection_bound line 404
  43. def OAI.NaimarkZFC.KOS.gramResidual line 441
  44. lemma OAI.NaimarkZFC.KOS.gramResidual_apply line 446
  45. theorem OAI.NaimarkZFC.KOS.gram_difference_projection_bound line 453
  46. theorem OAI.NaimarkZFC.KOS.approximate_gram_projection line 496
  47. theorem OAI.NaimarkZFC.KOS.finite_projection_positive_lift line 567
  48. theorem OAI.NaimarkZFC.KOS.approximate_gram_positive_lift line 581
  49. theorem OAI.NaimarkZFC.KOS.resolvent_commutator line 611
  50. lemma OAI.NaimarkZFC.KOS.resolvent_commutator_norm line 627
  51. lemma OAI.NaimarkZFC.KOS.saCayley_affine_resolvent line 638
  52. theorem OAI.NaimarkZFC.KOS.saCayley_commutator_norm line 650
  53. theorem OAI.NaimarkZFC.KOS.exact_gram_positive_lift line 666
  54. def OAI.NaimarkZFC.KOS.projectionSwitch line 697
  55. lemma OAI.NaimarkZFC.KOS.projectionSwitch_unitary line 699
  56. lemma OAI.NaimarkZFC.KOS.projectionSwitch_eq line 704
  57. lemma OAI.NaimarkZFC.KOS.projectionSwitch_sub_one line 714
  58. lemma OAI.NaimarkZFC.KOS.projectionSwitch_add_one line 736
  59. lemma OAI.NaimarkZFC.KOS.projectionSwitch_commutator_norm line 758
  60. lemma OAI.NaimarkZFC.KOS.projectionSwitch_fixed_error line 770
  61. lemma OAI.NaimarkZFC.KOS.projectionSwitch_negated_error line 788
  62. lemma OAI.NaimarkZFC.KOS.projectionSwitch_vector_error line 813
  63. lemma OAI.NaimarkZFC.KOS.unitary_commutator_product line 829
  64. theorem OAI.NaimarkZFC.KOS.corrected_projectionSwitch line 842
  65. def OAI.NaimarkZFC.KOS.rowAverage line 881
  66. lemma OAI.NaimarkZFC.KOS.rowAverage_selfAdjoint line 883
  67. lemma OAI.NaimarkZFC.KOS.rowAverage_apply line 888
  68. lemma OAI.NaimarkZFC.KOS.rowAverage_apply_one line 893
  69. lemma OAI.NaimarkZFC.KOS.rowAverage_error line 898
  70. lemma OAI.NaimarkZFC.KOS.rowAverage_small line 914
  71. lemma OAI.NaimarkZFC.KOS.rowAverage_pair_error line 926
  72. theorem OAI.NaimarkZFC.KOS.orthogonal_row_interchange line 947
  73. lemma OAI.NaimarkZFC.KOS.near_congruence_operator line 989
  74. lemma OAI.NaimarkZFC.KOS.irreducible_near_congruence line 1070
  75. lemma OAI.NaimarkZFC.KOS.rowAverage_pair_error_approx line 1118
  76. theorem OAI.NaimarkZFC.KOS.orthogonal_row_interchange_approx line 1139
  77. def OAI.NaimarkZFC.KOS.rowDefectTest line 1184
  78. def OAI.NaimarkZFC.KOS.rowFrameTests line 1187
  79. lemma OAI.NaimarkZFC.KOS.gram_mem_rowFrameTests line 1191
  80. lemma OAI.NaimarkZFC.KOS.defect_mem_rowFrameTests line 1196
  81. lemma OAI.NaimarkZFC.KOS.row_frame_coefficient line 1201
  82. lemma OAI.NaimarkZFC.KOS.row_defect_coefficient line 1207
  83. lemma OAI.NaimarkZFC.KOS.row_defect_zero line 1213
  84. lemma OAI.NaimarkZFC.KOS.row_defect_bound line 1220
  85. lemma OAI.NaimarkZFC.KOS.unitary_commutator_star line 1228
  86. lemma OAI.NaimarkZFC.KOS.unitary_commutator_sum line 1243
  87. def OAI.NaimarkZFC.KOS.upperCutoff line 1258
  88. lemma OAI.NaimarkZFC.KOS.continuous_upperCutoff line 1260
  89. lemma OAI.NaimarkZFC.KOS.upperCutoff_positive_form line 1264
  90. lemma OAI.NaimarkZFC.KOS.upperCutoff_range_lower line 1282
  91. theorem OAI.NaimarkZFC.KOS.upperCutoff_finiteDimensional_range line 1309
  92. lemma OAI.NaimarkZFC.KOS.isCompactOperator_of_finiteDimensional_range line 1338
  93. def OAI.NaimarkZFC.KOS.compactPreimageIdeal line 1351
  94. lemma OAI.NaimarkZFC.KOS.compactPreimageIdeal_isClosed line 1359
  95. lemma OAI.NaimarkZFC.KOS.mem_compactPreimageIdeal line 1366
  96. theorem OAI.NaimarkZFC.KOS.simple_infinite_no_compacts line 1370
  97. theorem OAI.NaimarkZFC.KOS.no_compacts_large_vector line 1387
  98. theorem OAI.NaimarkZFC.KOS.pure_vector_approximation_orthogonal line 1439
  99. theorem OAI.NaimarkZFC.KOS.third_vector_two_frames line 1490
  100. theorem OAI.NaimarkZFC.KOS.row_controlled_matching line 1529