OAI/Analysis/BoundedHochschild/CenterExpectations.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The center-valued conditional expectation and its normality.

  1. lemma OAI.HochschildCentralQuantization.central_trace_unique line 26
  2. lemma OAI.HochschildCentralQuantization.exists_unique_center_part line 34
  3. def OAI.HochschildCentralQuantization.centerPart line 40
  4. lemma OAI.HochschildCentralQuantization.centerPart_norm line 42
  5. lemma OAI.HochschildCentralQuantization.centerPart_central line 45
  6. lemma OAI.HochschildCentralQuantization.centerPart_trace line 48
  7. lemma OAI.HochschildCentralQuantization.centerPart_add line 52
  8. lemma OAI.HochschildCentralQuantization.centerPart_smul line 62
  9. def OAI.HochschildCentralQuantization.centerExpectation line 71
  10. lemma OAI.HochschildCentralQuantization.centerExpectation_apply line 80
  11. lemma OAI.HochschildCentralQuantization.centerExpectation_fix line 83
  12. lemma OAI.HochschildCentralQuantization.centerExpectation_bimodule line 88
  13. lemma OAI.HochschildCentralQuantization.centered_sub_expectation line 97
  14. lemma OAI.HochschildCentralQuantization.centerExpectation_idempotent line 102
  15. lemma OAI.HochschildCentralQuantization.centerExpectation_zero_iff line 107
  16. lemma OAI.HochschildCentralQuantization.centerExpectation_star line 121
  17. lemma OAI.HochschildCentralQuantization.centerExpectation_trace_adjoint line 133
  18. lemma OAI.HochschildCentralQuantization.centerExpectation_normal line 148
  19. lemma OAI.HochschildCentralQuantization.centerExpectation_norm_le line 156
  20. lemma OAI.HochschildCentralQuantization.centerExpectation_nonneg line 162