OAI/Analysis/CStarAlgebra/PureInfiniteness/Hereditary.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MainGap.sandwichAlgebra line 13
  2. def OAI.MainGap.Her line 29
  3. lemma OAI.MainGap.mem_Her_iff line 31
  4. lemma OAI.MainGap.isClosed_Her line 34
  5. instance OAI.MainGap.(instance at line 36) line 36
  6. lemma OAI.MainGap.sandwich_mem_Her line 38
  7. instance OAI.MainGap.(instance at line 41) line 41
  8. def OAI.MainGap.sandwichMap line 43
  9. lemma OAI.MainGap.sandwichMap_val line 52
  10. lemma OAI.MainGap.sandwichMap_dense line 54
  11. lemma OAI.MainGap.norm_mul_eq_of_star_mul_eq line 68
  12. def OAI.MainGap.carrierNumerator line 78
  13. def OAI.MainGap.carrier line 83
  14. lemma OAI.MainGap.carrier_on_sandwich line 86
  15. lemma OAI.MainGap.carrier_norm line 93
  16. lemma OAI.MainGap.carrier_inner line 100
  17. lemma OAI.MainGap.carrier_mul line 113
  18. lemma OAI.MainGap.norm_mul_star_eq_of_star_mul_eq line 127
  19. lemma OAI.MainGap.norm_sandwich_eq line 136
  20. def OAI.MainGap.conjugationNumerator line 141
  21. def OAI.MainGap.conjugation line 146
  22. lemma OAI.MainGap.conjugation_on_sandwich line 149
  23. lemma OAI.MainGap.conjugation_norm line 156
  24. lemma OAI.MainGap.conjugation_mem line 162
  25. lemma OAI.MainGap.conjugation_mul line 170
  26. lemma OAI.MainGap.carrier_outer line 189
  27. lemma OAI.MainGap.conjugation_star line 203
  28. def OAI.MainGap.transportHom line 215
  29. lemma OAI.MainGap.transportHom_injective line 221
  30. lemma OAI.MainGap.transport_represented_norm line 231
  31. lemma OAI.MainGap.Her_sandwich line 242
  32. lemma OAI.MainGap.Her_mono_of_mem line 252
  33. lemma OAI.MainGap.Her_mul_le line 257
  34. structure OAI.MainGap.RegularTransport line 264
  35. def OAI.MainGap.RegularTransport.restrict line 275
  36. lemma OAI.MainGap.RegularTransport.carrier_represented_norm line 297
  37. lemma OAI.MainGap.RegularTransport.represented_norm line 302
  38. lemma OAI.MainGap.RegularTransport.norm_hom line 316
  39. lemma OAI.MainGap.RegularTransport.injective line 319
  40. lemma OAI.MainGap.mul_star_mem_Her line 331
  41. lemma OAI.MainGap.sqrt_mem_Her line 336
  42. lemma OAI.MainGap.self_mem_Her line 340
  43. lemma OAI.MainGap.sqrt_Her_eq line 347
  44. def OAI.MainGap.twoSidedRemainder line 355
  45. lemma OAI.MainGap.twoSidedRemainder_as_square line 357
  46. lemma OAI.MainGap.twoSidedRemainder_nonneg line 369
  47. lemma OAI.MainGap.twoSidedRemainder_mono line 374
  48. lemma OAI.MainGap.norm_twoSidedRemainder_le line 382
  49. lemma OAI.MainGap.norm_sqrt_remainder_sq_le line 393
  50. lemma OAI.MainGap.norm_compression_error_le line 404
  51. lemma OAI.MainGap.norm_compression_error_sq_le line 423
  52. lemma OAI.MainGap.Her_exists_approx_unit line 439
  53. lemma OAI.MainGap.mem_Her_of_nonneg_le line 457
  54. lemma OAI.MainGap.Her_mono line 478
  55. lemma OAI.MainGap.real_smul_mem_Her line 482
  56. lemma OAI.MainGap.smul_Her_eq line 486
  57. lemma OAI.MainGap.square_Her_eq line 494
  58. lemma OAI.MainGap.Her_eq_of_order_bounds line 499
  59. def OAI.MainGap.cut line 506
  60. lemma OAI.MainGap.cut_nonneg line 508
  61. lemma OAI.MainGap.cut_mem_Her line 511
  62. lemma OAI.MainGap.cut_sandwich_lower line 514
  63. lemma OAI.MainGap.cut_transport_lower line 540
  64. theorem OAI.MainGap.regularTransport_of_approx line 559