OAI/Analysis/FactorGeneration/RepresentedCorners.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

The actual corner on pH. Extension by zero identifies its operators with supported ambient operators; weak closedness is proved by WOT continuity.

  1. def OAI.Generator.Tracial.cornerSpace line 16
  2. theorem OAI.Generator.Tracial.mem_cornerSpace line 22
  3. instance OAI.Generator.Tracial.cornerSpace_complete line 24
  4. def OAI.Generator.Tracial.cornerProject line 28
  5. theorem OAI.Generator.Tracial.cornerProject_coe line 33
  6. theorem OAI.Generator.Tracial.cornerProject_subtype line 34
  7. theorem OAI.Generator.Tracial.cornerProject_inner line 37
  8. def OAI.Generator.Tracial.cornerExtend line 43
  9. theorem OAI.Generator.Tracial.cornerExtend_apply line 46
  10. theorem OAI.Generator.Tracial.cornerExtend_zero line 49
  11. theorem OAI.Generator.Tracial.cornerExtend_add line 50
  12. theorem OAI.Generator.Tracial.cornerExtend_smul line 52
  13. theorem OAI.Generator.Tracial.cornerExtend_one line 54
  14. theorem OAI.Generator.Tracial.cornerExtend_mul line 55
  15. theorem OAI.Generator.Tracial.cornerExtend_star line 60
  16. theorem OAI.Generator.Tracial.cornerExtend_injective line 73
  17. theorem OAI.Generator.Tracial.cornerExtend_left line 79
  18. theorem OAI.Generator.Tracial.cornerExtend_right line 84
  19. def OAI.Generator.Tracial.cornerStarAlgebra line 88
  20. theorem OAI.Generator.Tracial.cornerExtend_wot_continuous line 99
  21. theorem OAI.Generator.Tracial.cornerStarAlgebra_wotClosed line 106
  22. def OAI.Generator.Tracial.representedCorner line 109
  23. def OAI.Generator.Tracial.cornerEmbedding line 112
  24. theorem OAI.Generator.Tracial.cornerEmbedding_injective line 120
  25. theorem OAI.Generator.Tracial.cornerEmbedding_one line 124
  26. theorem OAI.Generator.Tracial.cornerEmbedding_left line 126
  27. theorem OAI.Generator.Tracial.cornerEmbedding_right line 128
  28. def OAI.Generator.Tracial.cornerCompressOperator line 133
  29. theorem OAI.Generator.Tracial.cornerCompressOperator_apply line 136
  30. theorem OAI.Generator.Tracial.cornerExtend_compress line 139
  31. theorem OAI.Generator.Tracial.cornerCompress_extend line 142
  32. def OAI.Generator.Tracial.cornerCompress line 147
  33. theorem OAI.Generator.Tracial.cornerEmbedding_compress line 153
  34. theorem OAI.Generator.Tracial.cornerCompress_embedding line 156
  35. theorem OAI.Generator.Tracial.cornerEmbedding_range line 159
  36. theorem OAI.Generator.Tracial.corner_norm₂_pos line 176
  37. def OAI.Generator.Tracial.normalizedCornerVector line 179
  38. theorem OAI.Generator.Tracial.normalizedCornerVector_norm line 182
  39. theorem OAI.Generator.Tracial.normalizedCornerVector_pairing line 188
  40. def OAI.Generator.Tracial.representedCornerTrace line 197
  41. theorem OAI.Generator.Tracial.representedCornerTrace_norm₂ line 215
  42. theorem OAI.Generator.Tracial.representedCornerTrace_trace line 223
  43. def OAI.Generator.Tracial.projectionInSubalgebra line 241
  44. def OAI.Generator.Tracial.representedSubcorner line 246

    Source documentation

    Both corners act on the same pH; only the membership predicate changes.

    def representedSubcorner (hpN : p.val.val ∈ N) : VonNeumannAlgebra (cornerSpace p) :=
…

    Mentions: OAI.Generator.Tracial.cornerSpace

  45. theorem OAI.Generator.Tracial.representedSubcorner_le line 249
  46. theorem OAI.Generator.Tracial.representedCorner_diffuse line 252
  47. theorem OAI.Generator.Tracial.representedCorner_irreducible line 286
  48. theorem OAI.Generator.Tracial.representedCorner_factor line 316
  49. theorem OAI.Generator.Tracial.representedCorner_separable line 324
  50. def OAI.Generator.Tracial.CornerPartition.fromRepresentedCorner line 349
  51. theorem OAI.Generator.Tracial.CornerPartition.fromRepresentedCorner_pinch line 360
  52. theorem OAI.Generator.Tracial.CornerPartition.fromRepresentedCorner_pinch_compress line 367
  53. theorem OAI.Generator.Tracial.CornerPartition.fromRepresentedCorner_mem line 378
  54. theorem OAI.Generator.Tracial.CornerPartition.fromRepresentedCorner_energy line 382
  55. theorem OAI.Generator.Tracial.exists_irreducible_corner_zero_trace_partition line 410
  56. theorem OAI.Generator.Tracial.exists_irreducible_corner_centered_partition line 435
  57. theorem OAI.Generator.Tracial.exists_irreducible_corner_local_piece line 447