OAI/Analysis/TracialSplitting/ProjectionFrames.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentMain.finiteSandwichIdeal line 26
  2. theorem OAI.CurrentMain.mem_finiteSandwichIdeal line 52
  3. theorem OAI.CurrentMain.exists_finite_fullness_approximation line 57
  4. theorem OAI.CurrentMain.exists_finite_fullness_identity line 74
  5. lemma OAI.CurrentMain.star_add_mul_add_le line 90
  6. lemma OAI.CurrentMain.list_square_sum_nonneg line 98
  7. lemma OAI.CurrentMain.finite_product_sum_bound line 104
  8. theorem OAI.CurrentMain.finite_gram_isUnit line 137
  9. theorem OAI.CurrentMain.exists_positive_fullness_frame line 148
  10. def OAI.CurrentMain.ProjectionSubequivalent line 188
  11. lemma OAI.CurrentMain.partialIsometry_right_support line 191
  12. lemma OAI.CurrentMain.ProjectionSubequivalent.refl line 202
  13. lemma OAI.CurrentMain.ProjectionSubequivalent.zero line 206
  14. lemma OAI.CurrentMain.ProjectionSubequivalent.trans line 209
  15. lemma OAI.CurrentMain.ProjectionSubequivalent.of_le line 223
  16. lemma OAI.CurrentMain.ProjectionSubequivalent.final_projection line 228
  17. lemma OAI.CurrentMain.ProjectionSubequivalent.trace_le line 237
  18. lemma OAI.CurrentMain.exists_corner_normalizer line 245
  19. lemma OAI.CurrentMain.projectionSubequivalent_of_compression line 267
  20. lemma OAI.CurrentMain.exists_spectral_cut line 276
  21. lemma OAI.CurrentMain.ProjectionCorner.coe_mul_compress_mul line 303
  22. lemma OAI.CurrentMain.exists_column_cut line 311
  23. theorem OAI.CurrentMain.split_column line 333
  24. lemma OAI.CurrentMain.mul_eq_zero_of_supports line 424
  25. lemma OAI.CurrentMain.projection_mul_zero_symm line 431
  26. lemma OAI.CurrentMain.ProjectionSubequivalent.range line 436
  27. lemma OAI.CurrentMain.ProjectionSubequivalent.orthogonal_add line 444
  28. lemma OAI.CurrentMain.comparison_pair line 464