OAI/Analysis/JiangSu/Traceless/TracelessPureInfiniteness.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentMain.Traceless.sandwichSubalgebra line 16
  2. def OAI.CurrentMain.Traceless.hereditaryCorner line 26
  3. theorem OAI.CurrentMain.Traceless.coe_hereditaryCorner line 29
  4. theorem OAI.CurrentMain.Traceless.self_mem_hereditaryCorner line 32
  5. theorem OAI.CurrentMain.Traceless.sqrt_mem_hereditaryCorner line 35
  6. theorem OAI.CurrentMain.Traceless.hereditaryCorner_sandwich line 39
  7. theorem OAI.CurrentMain.Traceless.sqrt_sandwich_mem_hereditaryCorner line 51
  8. theorem OAI.CurrentMain.Traceless.hereditaryCorner_le_of_mem line 56
  9. theorem OAI.CurrentMain.Traceless.hereditaryCorner_mul_eq_zero line 64
  10. lemma OAI.CurrentMain.Traceless.cfc_mem_hereditaryCorner line 77
  11. theorem OAI.CurrentMain.Traceless.orthogonal_pair_of_positive_spectral_values line 84
  12. theorem OAI.CurrentMain.Traceless.positive_scalar_projection_or_orthogonal_pair line 132
  13. lemma OAI.CurrentMain.Traceless.hereditary_projection_right_identity line 180
  14. lemma OAI.CurrentMain.Traceless.scalar_of_no_orthogonal_pair line 187
  15. lemma OAI.CurrentMain.Traceless.scalar_sandwich_of_positive_sandwich line 213
  16. theorem OAI.CurrentMain.Traceless.exists_orthogonal_positive_pair line 230
  17. theorem OAI.CurrentMain.Traceless.exists_hereditary_isometry_range line 257
  18. def OAI.CurrentMain.Traceless.IsInfiniteProjection line 294
  19. theorem OAI.CurrentMain.Traceless.isInfiniteProjection_of_isometry line 298
  20. theorem OAI.CurrentMain.Traceless.infinite_projection_in_every_hereditary line 349