OAI/Analysis/BoundedHochschild/Haagerup.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Free-group convolution bounds and transfer of Haagerup estimates to tracial algebras.

  1. abbrev OAI.HochschildLength.Word line 16
  2. def OAI.HochschildLength.words line 17
  3. lemma OAI.HochschildLength.mem_words line 20
  4. def OAI.HochschildLength.wordBall line 27
  5. lemma OAI.HochschildLength.mem_wordBall line 28
  6. lemma OAI.HochschildLength.reduced_boundary_product line 35
  7. lemma OAI.HochschildLength.boundary_unique line 45
  8. lemma OAI.HochschildLength.append_injOn line 64
  9. lemma OAI.HochschildLength.invRev_append_injOn line 76
  10. lemma OAI.HochschildLength.sum_sq_comp_le line 90
  11. lemma OAI.HochschildLength.coefficient_energy_le line 111
  12. lemma OAI.HochschildLength.input_energy_le line 121
  13. def OAI.HochschildLength.piece line 133
  14. lemma OAI.HochschildLength.piece_norm_sq_le line 138
  15. lemma OAI.HochschildLength.piece_norm_le line 156
  16. lemma OAI.HochschildLength.single_sum line 172
  17. def OAI.HochschildLength.tripleBox line 179
  18. def OAI.HochschildLength.triples line 184
  19. lemma OAI.HochschildLength.mem_triples line 187
  20. def OAI.HochschildLength.tripleValue line 193
  21. def OAI.HochschildLength.triplePair line 197
  22. def OAI.HochschildLength.convolution line 200
  23. lemma OAI.HochschildLength.sum_pieces line 204
  24. lemma OAI.HochschildLength.convolution_eq_pieces line 219
  25. theorem OAI.HochschildLength.convolution_norm_le line 274
  26. abbrev OAI.HochschildTransfer.Polynomial line 299
  27. def OAI.HochschildTransfer.vector line 301
  28. lemma OAI.HochschildTransfer.vector_def line 305
  29. lemma OAI.HochschildTransfer.vector_single line 309
  30. lemma OAI.HochschildTransfer.vector_norm_sq line 313
  31. def OAI.HochschildTransfer.wordCoeff line 318
  32. lemma OAI.HochschildTransfer.wordCoeff_toWord line 322
  33. lemma OAI.HochschildTransfer.reduced_of_wordCoeff_ne_zero line 327
  34. lemma OAI.HochschildTransfer.wordCoeff_eq_zero line 334
  35. lemma OAI.HochschildTransfer.sum_wordCoeff line 338
  36. lemma OAI.HochschildTransfer.polynomial_wordSum line 364
  37. lemma OAI.HochschildTransfer.vector_wordSum line 370
  38. lemma OAI.HochschildTransfer.vector_mul_wordSum line 375
  39. lemma OAI.HochschildTransfer.vector_norm_sq_wordSum line 385
  40. lemma OAI.HochschildTransfer.vector_mul_norm_le line 392
  41. lemma OAI.HochschildTracePolynomial.inner_word line 439
  42. lemma OAI.HochschildTracePolynomial.norm_sum_word_sq line 450
  43. lemma OAI.HochschildTracePolynomial.norm_eval_sq line 469
  44. def OAI.HochschildPolynomial.adjoint line 483
  45. lemma OAI.HochschildPolynomial.coeff_adjoint line 486
  46. lemma OAI.HochschildPolynomial.adjoint_support line 492
  47. lemma OAI.HochschildPolynomial.eval_adjoint line 497
  48. lemma OAI.HochschildTransfer.vector_norm_eq_preGNS line 522
  49. lemma OAI.HochschildTransfer.norm_one_gns line 528
  50. lemma OAI.HochschildTransfer.norm_star_gns line 535
  51. theorem OAI.HochschildTransfer.norm_eval_homogeneous_le line 545