OAI/Analysis/CStarAlgebra/PureInfiniteness/Graph.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MainGap.OrthogonalSlots.graphWord line 15
  2. lemma OAI.MainGap.OrthogonalSlots.graphWord_inner line 18
  3. lemma OAI.MainGap.OrthogonalSlots.graphWord_outer line 27
  4. lemma OAI.MainGap.OrthogonalSlots.slot_graphWord line 33
  5. lemma OAI.MainGap.OrthogonalSlots.graphWord_mul line 40
  6. lemma OAI.MainGap.cfc_mul_mem_Her line 57
  7. def OAI.MainGap.graphComplement line 69
  8. lemma OAI.MainGap.graphComplement_nonneg line 72
  9. lemma OAI.MainGap.graphComplement_mul_self line 75
  10. lemma OAI.MainGap.graphComplement_mul_mem line 106
  11. def OAI.MainGap.graphCoeffs line 112
  12. lemma OAI.MainGap.graphCoeffs_inner line 116
  13. lemma OAI.MainGap.graphCoeffs_mem line 127
  14. lemma OAI.MainGap.Her_fixed_right line 138
  15. def OAI.MainGap.graphInverseFn line 145
  16. lemma OAI.MainGap.continuous_graphInverseFn line 147
  17. lemma OAI.MainGap.graphInverseFn_zero line 153
  18. def OAI.MainGap.graphInverse line 155
  19. lemma OAI.MainGap.graphInverse_mem line 161
  20. lemma OAI.MainGap.cut_mul_graphInverse line 164
  21. lemma OAI.MainGap.right_fixed_by_graphInverse line 185
  22. lemma OAI.MainGap.map_graphInverse line 189
  23. lemma OAI.MainGap.positive_mul_zero_of_conjugate_zero line 199
  24. lemma OAI.MainGap.positive_fixed_of_square_fixed line 210
  25. lemma OAI.MainGap.sqrt_fixed_of_fixed line 217
  26. lemma OAI.MainGap.star_mul_le_one_of_norm_le_one line 221
  27. lemma OAI.MainGap.graph_defect_forces line 226
  28. lemma OAI.MainGap.norm_conjugate_eq_of_isometric_on line 256
  29. def OAI.MainGap.graphSlot line 276
  30. def OAI.MainGap.graphZ line 278
  31. def OAI.MainGap.graphP line 281
  32. lemma OAI.MainGap.graphZ_inner line 284
  33. lemma OAI.MainGap.graphP_nonneg line 289
  34. lemma OAI.MainGap.graphP_mem line 292
  35. lemma OAI.MainGap.graphP_represented_norm line 295
  36. lemma OAI.MainGap.slot_sandwich_mem line 302
  37. def OAI.MainGap.graphX line 314
  38. def OAI.MainGap.graphB line 316
  39. lemma OAI.MainGap.graphX_nonneg line 319
  40. lemma OAI.MainGap.graphX_mem line 323
  41. lemma OAI.MainGap.graphB_mem line 327
  42. lemma OAI.MainGap.graphSlot0_Z line 331
  43. lemma OAI.MainGap.graphSlot_Z line 336
  44. lemma OAI.MainGap.norm_compression_eq_of_fixed line 343
  45. theorem OAI.MainGap.graph_failure line 362
  46. def OAI.MainGap.measurementX line 443
  47. def OAI.MainGap.measurementB line 444
  48. theorem OAI.MainGap.graph_failure_of_identities line 447
  49. lemma OAI.MainGap.graph_map_real_smul line 528
  50. lemma OAI.MainGap.graph_map_inverse line 531
  51. lemma OAI.MainGap.graphX_map line 535
  52. lemma OAI.MainGap.graphB_map line 539
  53. theorem OAI.MainGap.graph_failure_represented line 544
  54. theorem OAI.MainGap.graph_nonvanishing line 590