OAI/Analysis/BoundedHochschild/HarmonicSums.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Harmonic sine estimates, Fourier windows, tracial Hilbert spaces and unitary power rigidity.

  1. theorem OAI.HochschildRigidity.norm_sum_smul_le_of_antitone line 14
  2. theorem OAI.HochschildRigidity.abs_sum_sin_le line 44
  3. theorem OAI.HochschildRigidity.abs_harmonic_sin_tail_le line 65
  4. theorem OAI.HochschildRigidity.abs_harmonic_sin_prefix_le line 84
  5. theorem OAI.HochschildRigidity.abs_harmonic_sin_le_pos line 101
  6. theorem OAI.HochschildRigidity.abs_harmonic_sin_le line 144
  7. def OAI.HochschildRigidity.harmonicPolynomial line 155
  8. theorem OAI.HochschildRigidity.harmonicPolynomial_im line 160
  9. theorem OAI.HochschildRigidity.norm_harmonicPolynomial_sub_star_le line 179
  10. theorem OAI.HochschildRigidity.norm_unitary_harmonicPolynomial_sub_star_le line 190
  11. lemma OAI.HochschildRigidity.sum_stdAddChar_mul line 219
  12. theorem OAI.HochschildRigidity.sum_dft_mul_star_dft line 226
  13. def OAI.HochschildRigidity.rootUnitary line 241
  14. lemma OAI.HochschildRigidity.rootUnitary_coe line 247
  15. def OAI.HochschildRigidity.fourierWindow line 250
  16. lemma OAI.HochschildRigidity.sum_fourierWindow_mul_star line 254
  17. lemma OAI.HochschildRigidity.sum_zmod_val line 266
  18. lemma OAI.HochschildRigidity.fourierWindow_eq_geometric line 272
  19. lemma OAI.HochschildRigidity.norm_unitary_mul_fourierWindow_sub_le line 288
  20. lemma OAI.HochschildRigidity.norm_unitary_pow_mul_sub_le line 306
  21. lemma OAI.HochschildRigidity.norm_star_unitary_mul_sub line 323
  22. lemma OAI.HochschildRigidity.norm_harmonicPolynomial_mul_sub_le line 329
  23. lemma OAI.HochschildRigidity.star_harmonicPolynomial line 353
  24. lemma OAI.HochschildRigidity.power_multiplier_smul line 358
  25. lemma OAI.HochschildRigidity.map_harmonicPolynomial line 364
  26. lemma OAI.HochschildRigidity.preGNS_norm_mul_le line 376
  27. lemma OAI.HochschildRigidity.preGNS_norm_one line 386
  28. lemma OAI.HochschildRigidity.preGNS_norm_le line 391
  29. lemma OAI.HochschildRigidity.preGNS_norm_star line 393
  30. lemma OAI.HochschildRigidity.preGNS_norm_mul_right_le line 400
  31. lemma OAI.HochschildRigidity.preGNS_norm_eq_zero_iff line 405
  32. lemma OAI.HochschildRigidity.sum_preGNS_norm_mul_sq line 419
  33. def OAI.HochschildRigidity.gnsFamily line 433
  34. lemma OAI.HochschildRigidity.norm_gnsFamily_sq line 436
  35. lemma OAI.HochschildRigidity.gnsFamily_add line 441
  36. lemma OAI.HochschildRigidity.gnsFamily_sub line 447
  37. lemma OAI.HochschildRigidity.gnsFamily_smul line 453
  38. lemma OAI.HochschildRigidity.norm_gnsFamily_mul line 458
  39. lemma OAI.HochschildRigidity.norm_gnsFamily_leftMul_le line 464
  40. lemma OAI.HochschildRigidity.norm_gnsFamily_sq_le line 475
  41. lemma OAI.HochschildRigidity.norm_gnsFamily_square_card_le line 486
  42. lemma OAI.HochschildRigidity.norm_gnsFamily_harmonic_error_le line 497
  43. theorem OAI.HochschildRigidity.unitary_power_multiplier_bound line 511
  44. theorem OAI.HochschildRigidity.unitary_power_rigidity line 583