OAI/Analysis/BoundedHochschild/TraceExpectations.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Trace pairing norms, predual vectors and trace-preserving expectations.

  1. lemma OAI.HochschildTraceNorm.norm_mul_eq_abs_mul line 27
  2. theorem OAI.HochschildTraceNorm.exists_approx_polar line 37
  3. def OAI.HochschildTraceNorm.traceCLM line 113
  4. lemma OAI.HochschildTraceNorm.traceCLM_apply line 117
  5. lemma OAI.HochschildTraceNorm.positive_weight_trace_bound line 120
  6. lemma OAI.HochschildTraceNorm.trace_pair_bound line 141
  7. def OAI.HochschildTraceNorm.tracePair line 170
  8. lemma OAI.HochschildTraceNorm.tracePair_apply line 173
  9. theorem OAI.HochschildTraceNorm.norm_tracePair line 178
  10. lemma OAI.BoundedHochschild.predual_vector_ext line 221
  11. lemma OAI.BoundedHochschild.exists_trace_vector line 232
  12. def OAI.BoundedHochschild.traceVector line 239
  13. lemma OAI.BoundedHochschild.traceVector_spec line 242
  14. def OAI.BoundedHochschild.traceVectorLinear line 245
  15. lemma OAI.BoundedHochschild.traceVectorLinear_apply line 257
  16. lemma OAI.BoundedHochschild.norm_traceVector line 260
  17. lemma OAI.BoundedHochschild.traceVector_injective line 278
  18. lemma OAI.HochschildTraceNorm.map_cstar_abs line 299
  19. lemma OAI.HochschildTraceNorm.norm_tracePair_embedding line 308
  20. theorem OAI.BoundedHochschild.exists_trace_expectation_value line 332
  21. lemma OAI.BoundedHochschild.trace_pair_separates line 369
  22. theorem OAI.BoundedHochschild.exists_expected_embedding line 389