OAI/Analysis/BoundedHochschild/SeparablePrimitives.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Dense unitary bases, normal expectations and separable finite exactness.

  1. lemma OAI.BoundedHochschild.preGNS_sq_le_traceVector line 33
  2. theorem OAI.BoundedHochschild.exists_dense_unitary_base line 49
  3. theorem OAI.BoundedHochschild.primitive_of_separable_normal_finite_paths line 109
  4. lemma OAI.BoundedHochschild.denseRange_traceVector line 144
  5. theorem OAI.BoundedHochschild.exists_preadjoint_of_trace_adjoint line 195
  6. lemma OAI.BoundedHochschild.right_hasPreadjoint_of_left line 237
  7. lemma OAI.BoundedHochschild.trace_preserving_norm line 266
  8. theorem OAI.BoundedHochschild.exists_normal_expected_embedding line 278
  9. lemma OAI.BoundedHochschild.ExpectedEmbedding.restrict_curryRight line 324
  10. lemma OAI.BoundedHochschild.ExpectedEmbedding.restrict_last_normal line 337
  11. theorem OAI.BoundedHochschild.finite_exactness_of_separable_subalgebra line 357