OAI/Analysis/BoundedHochschild/Corners.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Spectral corners, corner preduals and factor structure.

  1. def OAI.HochschildCorners.corner line 39
  2. lemma OAI.HochschildCorners.mem_corner line 57
  3. instance OAI.HochschildCorners.corner_closed line 60
  4. lemma OAI.HochschildCorners.self_mem_corner line 65
  5. lemma OAI.HochschildCorners.projection_mem_corner line 68
  6. lemma OAI.HochschildCorners.compress_mem_corner line 73
  7. lemma OAI.HochschildCorners.posPart_mem_corner line 79
  8. lemma OAI.HochschildCorners.negPart_mem_corner line 84
  9. lemma OAI.HochschildCorners.support_le_corner line 88
  10. lemma OAI.HochschildCorners.exists_corner_dyadic_projection line 97
  11. lemma OAI.HochschildCorners.real_smul_mem_corner line 159
  12. theorem OAI.HochschildCorners.dual_zero_on_corner line 166
  13. lemma OAI.HochschildCorners.commute_corner_of_projections line 237
  14. abbrev OAI.HochschildCorners.Corner line 267
  15. instance OAI.HochschildCorners.cornerOne line 269
  16. lemma OAI.HochschildCorners.corner_coe_one line 271
  17. instance OAI.HochschildCorners.cornerRing line 273
  18. instance OAI.HochschildCorners.cornerAlgebra line 283
  19. instance OAI.HochschildCorners.cornerNormedRing line 302
  20. instance OAI.HochschildCorners.cornerNormedAlgebra line 307
  21. instance OAI.HochschildCorners.cornerCStarAlgebra line 309
  22. lemma OAI.HochschildCorners.corner_coe_mul line 312
  23. lemma OAI.HochschildCorners.corner_coe_star line 314
  24. lemma OAI.HochschildCorners.corner_coe_smul line 316
  25. lemma OAI.HochschildCorners.corner_coe_zero line 318
  26. example OAI.HochschildCorners.(example at line 320) line 320
  27. instance OAI.HochschildCorners.cornerStarOrderedRing line 321
  28. def OAI.HochschildCorners.weakCorner line 340
  29. lemma OAI.HochschildCorners.weakCorner_closed line 357
  30. def OAI.HochschildCorners.CornerPredual line 375
  31. instance OAI.HochschildCorners.(instance at line 376) line 376
  32. instance OAI.HochschildCorners.(instance at line 378) line 378
  33. instance OAI.HochschildCorners.(instance at line 380) line 380
  34. def OAI.HochschildCorners.cornerStrongEquiv line 383
  35. def OAI.HochschildCorners.cornerPredualEquiv line 397
  36. lemma OAI.HochschildCorners.cornerPredualEquiv_apply line 401
  37. lemma OAI.HochschildCorners.cornerPredualEquiv_symm_mk line 407
  38. lemma OAI.HochschildCorners.corner_projection_coe line 431
  39. lemma OAI.HochschildCorners.corner_projection_le line 435
  40. lemma OAI.HochschildCorners.corner_no_minimal line 438
  41. def OAI.HochschildCorners.cornerTrace line 453
  42. lemma OAI.HochschildCorners.cornerTrace_apply line 459
  43. lemma OAI.HochschildCorners.cornerTrace_one line 462
  44. lemma OAI.HochschildCorners.cornerTrace_tracial line 468
  45. lemma OAI.HochschildCorners.cornerTrace_faithful line 472
  46. lemma OAI.HochschildCorners.cornerTrace_normal line 479
  47. lemma OAI.HochschildCorners.corner_factor_of_matrix_diagonal line 506
  48. lemma OAI.HochschildCorners.exists_matrix_diagonal_below line 574
  49. lemma OAI.HochschildCorners.corner_factor line 596