OAI/Analysis/BoundedHochschild/WeakAlgebras.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Weak-star algebra closures, inherited traces and generated finite-path primitives.

  1. def OAI.BoundedHochschild.WeakAlgebra.weakEquiv line 31
  2. lemma OAI.BoundedHochschild.WeakAlgebra.weakEquiv_symm_continuous line 34
  3. lemma OAI.BoundedHochschild.WeakAlgebra.normal_continuous line 37
  4. lemma OAI.BoundedHochschild.WeakAlgebra.star_continuous line 46
  5. def OAI.BoundedHochschild.WeakAlgebra.linearClosure line 55
  6. lemma OAI.BoundedHochschild.WeakAlgebra.linearClosure_closed line 58
  7. lemma OAI.BoundedHochschild.WeakAlgebra.mem_linearClosure line 62
  8. lemma OAI.BoundedHochschild.WeakAlgebra.closure_stable line 66
  9. lemma OAI.BoundedHochschild.WeakAlgebra.mul_mem line 74
  10. lemma OAI.BoundedHochschild.WeakAlgebra.star_mem line 91
  11. def OAI.BoundedHochschild.WeakAlgebra.closure line 101
  12. instance OAI.BoundedHochschild.WeakAlgebra.closure_closed line 114
  13. def OAI.BoundedHochschild.WeakAlgebra.strongEquiv line 126
  14. def OAI.BoundedHochschild.WeakAlgebra.predualEquiv line 141
  15. instance OAI.BoundedHochschild.WeakAlgebra.closure_wstar line 147
  16. lemma OAI.BoundedHochschild.WeakAlgebra.predualEquiv_apply line 151
  17. lemma OAI.BoundedHochschild.WeakAlgebra.predualEquiv_symm_apply_mk line 159
  18. lemma OAI.BoundedHochschild.WeakAlgebra.inherited_left_normal line 166
  19. lemma OAI.BoundedHochschild.WeakAlgebra.inherited_right_normal line 177
  20. lemma OAI.BoundedHochschild.WeakAlgebra.traceVector_norm_bound line 208
  21. def OAI.BoundedHochschild.WeakAlgebra.traceRestriction line 219
  22. lemma OAI.BoundedHochschild.WeakAlgebra.traceRestriction_apply line 226
  23. lemma OAI.BoundedHochschild.WeakAlgebra.denseRange_traceRestriction line 233
  24. theorem OAI.BoundedHochschild.WeakAlgebra.separablePredual_of_separable line 289
  25. lemma OAI.BoundedHochschild.countable_submonoidClosure line 305
  26. lemma OAI.BoundedHochschild.separable_starAdjoin line 320
  27. instance OAI.BoundedHochschild.WeakAlgebra.closedSubalgebra_starOrderedRing line 343
  28. def OAI.BoundedHochschild.WeakAlgebra.inheritedTrace line 370
  29. lemma OAI.BoundedHochschild.WeakAlgebra.inheritedTrace_apply line 374
  30. lemma OAI.BoundedHochschild.WeakAlgebra.inheritedTrace_normal line 378
  31. lemma OAI.BoundedHochschild.WeakAlgebra.inheritedTrace_faithful line 385
  32. lemma OAI.BoundedHochschild.WeakAlgebra.inheritedTrace_tracial line 391
  33. lemma OAI.BoundedHochschild.WeakAlgebra.inheritedTrace_one line 396
  34. theorem OAI.BoundedHochschild.primitive_of_generated_finite_paths line 417