OAI/Analysis/Naimark/Operators.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NaimarkZFC.KOS.matrixRow line 15
  2. lemma OAI.NaimarkZFC.KOS.matrixRow_apply line 19
  3. lemma OAI.NaimarkZFC.KOS.matrixRow_gram line 23
  4. def OAI.NaimarkZFC.KOS.matrixConst line 29
  5. lemma OAI.NaimarkZFC.KOS.matrixConst_apply line 33
  6. lemma OAI.NaimarkZFC.KOS.matrixConst_norm line 36
  7. lemma OAI.NaimarkZFC.KOS.matrixConst_star line 40
  8. lemma OAI.NaimarkZFC.KOS.matrixConst_mul line 46
  9. lemma OAI.NaimarkZFC.KOS.matrixRow_average line 49
  10. lemma OAI.NaimarkZFC.KOS.matrixRow_average_norm line 54
  11. def OAI.NaimarkZFC.KOS.columnMap line 64
  12. lemma OAI.NaimarkZFC.KOS.columnMap_apply line 68
  13. lemma OAI.NaimarkZFC.KOS.columnMap_single line 71
  14. lemma OAI.NaimarkZFC.KOS.columnMap_adjoint_apply line 75
  15. def OAI.NaimarkZFC.KOS.matrixOperator line 80
  16. lemma OAI.NaimarkZFC.KOS.matrixOperator_apply line 84
  17. def OAI.NaimarkZFC.KOS.scalarGram line 87
  18. lemma OAI.NaimarkZFC.KOS.scalarGram_operator line 90
  19. lemma OAI.NaimarkZFC.KOS.scalarGram_norm line 97
  20. def OAI.NaimarkZFC.KOS.matrixScalar line 101
  21. lemma OAI.NaimarkZFC.KOS.matrixScalar_apply line 105
  22. lemma OAI.NaimarkZFC.KOS.matrixScalar_norm line 111
  23. lemma OAI.NaimarkZFC.KOS.matrixScalar_mul_const line 114
  24. lemma OAI.NaimarkZFC.KOS.excision_matrix_gram_tendsto line 119
  25. lemma OAI.NaimarkZFC.KOS.norm_lt_of_gram_approx line 145
  26. lemma OAI.NaimarkZFC.KOS.excision_matrix_row_norm line 161
  27. lemma OAI.NaimarkZFC.KOS.norm_sum_sq_of_orthogonal line 187
  28. lemma OAI.NaimarkZFC.KOS.projection_inner_zero line 199
  29. lemma OAI.NaimarkZFC.KOS.projection_family_sum_norm_sq_le line 206
  30. lemma OAI.NaimarkZFC.KOS.projection_blocks_norm_le line 234
  31. structure OAI.NaimarkZFC.KOS.ProjectionChain line 266
  32. def OAI.NaimarkZFC.KOS.ProjectionChain.block line 275
  33. lemma OAI.NaimarkZFC.KOS.ProjectionChain.reverse_increasing line 277
  34. lemma OAI.NaimarkZFC.KOS.ProjectionChain.block_projection line 282
  35. lemma OAI.NaimarkZFC.KOS.ProjectionChain.blocks_orthogonal line 291
  36. lemma OAI.NaimarkZFC.KOS.ProjectionChain.upper_block line 305
  37. lemma OAI.NaimarkZFC.KOS.ProjectionChain.commutator_block line 320
  38. def OAI.NaimarkZFC.KOS.ProjectionChain.average line 328
  39. lemma OAI.NaimarkZFC.KOS.ProjectionChain.sum_commutator_norm_le line 330
  40. lemma OAI.NaimarkZFC.KOS.ProjectionChain.average_commutator_norm_le line 347
  41. def OAI.NaimarkZFC.KOS.krylovSet line 363
  42. def OAI.NaimarkZFC.KOS.krylovSpace line 367
  43. instance OAI.NaimarkZFC.KOS.krylovSpace_finite line 370
  44. lemma OAI.NaimarkZFC.KOS.krylovSpace_mono line 375
  45. lemma OAI.NaimarkZFC.KOS.mem_krylovSpace line 383
  46. lemma OAI.NaimarkZFC.KOS.map_mem_krylovSpace line 388
  47. def OAI.NaimarkZFC.KOS.krylovChain line 403
  48. lemma OAI.NaimarkZFC.KOS.krylovChain_band line 409
  49. lemma OAI.NaimarkZFC.KOS.krylovChain_fixes line 417
  50. lemma OAI.NaimarkZFC.KOS.krylovAverage_fixes line 421
  51. lemma OAI.NaimarkZFC.KOS.krylovAverage_selfAdjoint line 427
  52. lemma OAI.NaimarkZFC.KOS.krylovAverage_norm line 433
  53. lemma OAI.NaimarkZFC.KOS.krylovAverage_mem line 445
  54. lemma OAI.NaimarkZFC.KOS.krylovAverage_projection line 454
  55. lemma OAI.NaimarkZFC.KOS.columnMap_comp line 472
  56. lemma OAI.NaimarkZFC.KOS.columnMap_sub line 477
  57. lemma OAI.NaimarkZFC.KOS.columnMap_matrix line 482
  58. def OAI.NaimarkZFC.KOS.basisColumn line 492
  59. lemma OAI.NaimarkZFC.KOS.basisColumn_apply line 495
  60. lemma OAI.NaimarkZFC.KOS.basisColumn_norm line 500
  61. lemma OAI.NaimarkZFC.KOS.basisColumn_projection line 507
  62. lemma OAI.NaimarkZFC.KOS.basisColumn_compression_selfAdjoint line 515
  63. lemma OAI.NaimarkZFC.KOS.compressedColumn_defect line 523
  64. lemma OAI.NaimarkZFC.KOS.krylov_column_reconstruct line 537
  65. theorem OAI.NaimarkZFC.KOS.finite_quasicentral_columns line 559
  66. lemma OAI.NaimarkZFC.KOS.matrixConst_mul_entry line 622
  67. lemma OAI.NaimarkZFC.KOS.matrix_mulConst_entry line 627
  68. lemma OAI.NaimarkZFC.KOS.scalar_const_commute line 632
  69. lemma OAI.NaimarkZFC.KOS.matrixRow_mul_scalar line 639
  70. lemma OAI.NaimarkZFC.KOS.matrixRow_defect line 647
  71. lemma OAI.NaimarkZFC.KOS.commutator_factorization line 659
  72. lemma OAI.NaimarkZFC.KOS.commutator_factorization_norm line 667
  73. lemma OAI.NaimarkZFC.KOS.rowAverage_commutator_norm line 679
  74. lemma OAI.NaimarkZFC.KOS.pureExcisionNet_strong line 708
  75. lemma OAI.NaimarkZFC.KOS.pureExcisionNet_squared_strong line 722
  76. lemma OAI.NaimarkZFC.KOS.excision_rowAverage_vector_tendsto line 742
  77. lemma OAI.NaimarkZFC.KOS.irreducible_vector_lift line 770
  78. theorem OAI.NaimarkZFC.KOS.approximate_matrix_rows_selfAdjoint line 780
  79. lemma OAI.NaimarkZFC.KOS.commutator_real_imaginary_norm line 842
  80. lemma OAI.NaimarkZFC.KOS.approximate_matrix_rows line 854
  81. lemma OAI.NaimarkZFC.KOS.commutator_congruence_norm_four line 879
  82. theorem OAI.NaimarkZFC.KOS.nearCentralRows line 898
  83. theorem OAI.NaimarkZFC.KOS.homogeneity line 927