OAI/Analysis/TracialSplitting/SpectralCutoffs.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.realSpectrum_finite line 22
  2. def OAI.CurrentMain.spectralAtom line 27
  3. lemma OAI.CurrentMain.spectralAtom_projection line 30
  4. lemma OAI.CurrentMain.spectralAtom_orthogonal line 40
  5. lemma OAI.CurrentMain.spectralAtom_sum line 54
  6. lemma OAI.CurrentMain.spectralAtom_resolution line 67
  7. lemma OAI.CurrentMain.spectralAtom_eigenvalue line 81
  8. def OAI.CurrentMain.projectionCornerSubalgebra line 98
  9. abbrev OAI.CurrentMain.ProjectionCorner line 117
  10. instance OAI.CurrentMain.ProjectionCorner.(instance at line 123) line 123
  11. instance OAI.CurrentMain.ProjectionCorner.(instance at line 129) line 129
  12. lemma OAI.CurrentMain.ProjectionCorner.coe_one line 133
  13. instance OAI.CurrentMain.ProjectionCorner.(instance at line 135) line 135
  14. instance OAI.CurrentMain.ProjectionCorner.(instance at line 138) line 138
  15. instance OAI.CurrentMain.ProjectionCorner.(instance at line 142) line 142
  16. lemma OAI.CurrentMain.ProjectionCorner.isClosed line 146
  17. instance OAI.CurrentMain.ProjectionCorner.(instance at line 150) line 150
  18. instance OAI.CurrentMain.ProjectionCorner.(instance at line 152) line 152
  19. def OAI.CurrentMain.ProjectionCorner.inclusion line 155
  20. lemma OAI.CurrentMain.ProjectionCorner.inclusion_isometric line 157
  21. lemma OAI.CurrentMain.ProjectionCorner.isSelfAdjoint_coe line 159
  22. lemma OAI.CurrentMain.ProjectionCorner.coe_cfc line 162
  23. lemma OAI.CurrentMain.ProjectionCorner.spectrum_coe_subset line 169
  24. def OAI.CurrentMain.ProjectionCorner.compress line 175
  25. lemma OAI.CurrentMain.ProjectionCorner.coe_compress line 181
  26. lemma OAI.CurrentMain.ProjectionCorner.coe_algebraMap line 183
  27. lemma OAI.CurrentMain.ProjectionCorner.spectrum_subset_coe line 186
  28. lemma OAI.CurrentMain.ProjectionCorner.finite_spectrum_of_coe line 212
  29. def OAI.CurrentMain.unitaryPolar line 227
  30. lemma OAI.CurrentMain.unitaryPolar_mem line 229
  31. lemma OAI.CurrentMain.unitaryPolar_one line 247
  32. lemma OAI.CurrentMain.continuousAt_unitaryPolar_one line 250
  33. lemma OAI.CurrentMain.commute_ring_inverse line 261
  34. def OAI.CurrentMain.projectionIntertwiner line 269
  35. lemma OAI.CurrentMain.projectionIntertwiner_self line 272
  36. lemma OAI.CurrentMain.projectionIntertwiner_mul line 279
  37. lemma OAI.CurrentMain.projectionIntertwiner_star line 293
  38. lemma OAI.CurrentMain.projectionIntertwiner_square_commute line 298
  39. lemma OAI.CurrentMain.unitaryPolar_intertwines line 307
  40. lemma OAI.CurrentMain.unitaryPolar_conjugates line 319
  41. def OAI.CurrentMain.gapCutoff line 331
  42. lemma OAI.CurrentMain.gapCutoff_continuous line 333
  43. lemma OAI.CurrentMain.gapCutoff_eq_zero line 337
  44. lemma OAI.CurrentMain.gapCutoff_eq_one line 341
  45. lemma OAI.CurrentMain.gapCutoff_zero line 345
  46. lemma OAI.CurrentMain.spectralCut_isProjection line 347
  47. lemma OAI.CurrentMain.complexSpectrum_finite line 360
  48. lemma OAI.CurrentMain.finite_spectrum_cfc line 365
  49. lemma OAI.CurrentMain.spectrum_shift_lower line 372
  50. lemma OAI.CurrentMain.cutoff_shift_corner line 388
  51. lemma OAI.CurrentMain.cutoff_shift_corner_gap line 402
  52. lemma OAI.CurrentMain.realRankZero_dense line 411
  53. lemma OAI.CurrentMain.spectrum_conjugate_unitary line 422
  54. lemma OAI.CurrentMain.projection_conjugate_compress line 426
  55. lemma OAI.CurrentMain.finite_spectrum_cut line 437
  56. lemma OAI.CurrentMain.realRankZero_corner line 446