OAI/Analysis/BoundedHochschild/CenterCorners.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Local central quantization and center-valued traces on corners.

  1. lemma OAI.HochschildCentralQuantization.exists_large_small_expectations line 28
  2. theorem OAI.HochschildCentralQuantization.exists_small_corner_of_trace_limit line 52
  3. theorem OAI.HochschildCentralQuantization.exists_small_corner line 118
  4. lemma OAI.HochschildCentralQuantization.exists_central_positive_cut line 143
  5. lemma OAI.HochschildCentralQuantization.centerExpectation_trace line 167
  6. lemma OAI.HochschildCentralQuantization.central_cut_compression line 173
  7. lemma OAI.HochschildCentralQuantization.central_cut_energy line 181
  8. lemma OAI.HochschildCentralQuantization.exists_center_order_cut line 192
  9. theorem OAI.HochschildCentralQuantization.exists_small_corner_center_order line 251
  10. lemma OAI.HochschildCentralQuantization.central_corner_projection_lift line 290
  11. lemma OAI.HochschildCentralQuantization.corner_selfAdjoint_posPart_trace line 313
  12. lemma OAI.HochschildCentralQuantization.corner_selfAdjoint_centered_zero line 336
  13. lemma OAI.HochschildCentralQuantization.corner_centered_zero line 358
  14. lemma OAI.HochschildCentralQuantization.central_corner_weight_mul line 389
  15. lemma OAI.HochschildCentralQuantization.central_corner_weight line 397
  16. lemma OAI.HochschildCentralQuantization.ambient_centered_corner line 410
  17. def OAI.HochschildCentralQuantization.cornerExpectation line 436
  18. lemma OAI.HochschildCentralQuantization.cornerExpectation_weighted_trace line 442
  19. lemma OAI.HochschildCentralQuantization.centerExpectation_corner_tower line 455
  20. lemma OAI.HochschildCentralQuantization.centerExpectation_monotone line 466
  21. lemma OAI.HochschildCentralQuantization.corner_typeII1 line 473