OAI/Analysis/TracialCohomology/BilinearModulus.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

Bilinear modulus for bounded Hochschild cohomology.

  1. theorem OAI.HochschildFourPoint.norm_exp_remainder line 18
  2. def OAI.HochschildFourPoint.twist line 62
  3. lemma OAI.HochschildFourPoint.twist_skew line 66
  4. lemma OAI.HochschildFourPoint.norm_twist_le line 72
  5. lemma OAI.HochschildFourPoint.phase_test line 79
  6. theorem OAI.HochschildFourPoint.four_phase_real_bound line 105
  7. theorem OAI.HochschildFourPoint.four_phase_dual_bound line 127
  8. def OAI.HochschildFourPoint.reRestrict line 181
  9. def OAI.HochschildFourPoint.imRestrict line 190
  10. def OAI.HochschildFourPoint.complexify line 199
  11. lemma OAI.HochschildFourPoint.norm_complexify_le line 205
  12. def OAI.HochschildFourPoint.complexifyCLM line 224
  13. lemma OAI.HochschildFourPoint.norm_complexifyCLM_le line 227
  14. lemma OAI.HochschildFourPoint.re_im_decompose line 231
  15. lemma OAI.HochschildFourPoint.norm_le_re_im line 242
  16. lemma OAI.HochschildFourPoint.norm_reRestrict_le_unitary_bound line 248
  17. lemma OAI.HochschildFourPoint.selfAdjoint_exp_test line 266
  18. lemma OAI.HochschildFourPoint.imRestrict_small line 292
  19. lemma OAI.HochschildFourPoint.near_unit_norm_bound line 311
  20. def OAI.HochschildFourPoint.unitSup line 321
  21. lemma OAI.HochschildFourPoint.unitSup_bdd line 324
  22. lemma OAI.HochschildFourPoint.le_unitSup line 330
  23. lemma OAI.HochschildFourPoint.unitSup_nonneg line 334
  24. def OAI.HochschildFourPoint.translate line 337
  25. lemma OAI.HochschildFourPoint.norm_translate line 340
  26. lemma OAI.HochschildFourPoint.translate_apply line 353
  27. theorem OAI.HochschildFourPoint.norm_le_of_unitary_bound line 356
  28. def OAI.HochschildFourPoint.absoluteSA line 405
  29. lemma OAI.HochschildFourPoint.absoluteSA_nonneg line 408
  30. lemma OAI.HochschildFourPoint.absoluteSA_sq line 412
  31. lemma OAI.HochschildFourPoint.norm_absoluteSA_le line 423
  32. lemma OAI.HochschildFourPoint.disk_contracts line 430
  33. lemma OAI.HochschildFourPoint.HochschildPositiveDecomposition.norm_pair_shift line 463
  34. def OAI.HochschildFourPoint.HochschildPositiveDecomposition.shiftEmbedding line 491
  35. lemma OAI.HochschildFourPoint.HochschildPositiveDecomposition.shiftEmbedding_injective line 496
  36. lemma OAI.HochschildFourPoint.HochschildPositiveDecomposition.exists_pair_extension line 508
  37. lemma OAI.HochschildFourPoint.HochschildPositiveDecomposition.norm_orderUnit_sub line 541
  38. lemma OAI.HochschildFourPoint.HochschildPositiveDecomposition.pair_nonneg line 551
  39. lemma OAI.HochschildFourPoint.HochschildPositiveDecomposition.exists_real_positive_difference line 566
  40. def OAI.HochschildFourPoint.HochschildPositiveDecomposition.complexify line 593
  41. lemma OAI.HochschildFourPoint.HochschildPositiveDecomposition.complexify_apply line 599
  42. lemma OAI.HochschildFourPoint.HochschildPositiveDecomposition.complexify_selfAdjoint line 602
  43. def OAI.HochschildFourPoint.HochschildPositiveDecomposition.complexifyPositive line 611
  44. lemma OAI.HochschildFourPoint.HochschildPositiveDecomposition.complexifyPositive_apply line 624
  45. def OAI.HochschildFourPoint.saSquare line 636
  46. lemma OAI.HochschildFourPoint.real_positive_square_bound line 641
  47. lemma OAI.HochschildFourPoint.real_positive_norm_le line 661
  48. lemma OAI.HochschildFourPoint.reRestrict_norm_le line 676
  49. lemma OAI.HochschildFourPoint.bilinear_sa_disk_bound line 688
  50. lemma OAI.HochschildFourPoint.exists_sa_modulus line 712
  51. def OAI.HochschildFourPoint.energySA line 740
  52. lemma OAI.HochschildFourPoint.energySA_eq line 745
  53. lemma OAI.HochschildFourPoint.square_nonneg line 754
  54. lemma OAI.HochschildFourPoint.complexifyCLM_sa line 759
  55. lemma OAI.HochschildFourPoint.exists_quartic_error line 768
  56. lemma OAI.HochschildFourPoint.bilinear_norm_le_of_unitary line 826
  57. lemma OAI.HochschildFourPoint.exists_unitary_pair line 837
  58. def OAI.HochschildFourPoint.translateB line 844
  59. lemma OAI.HochschildFourPoint.translateB_apply line 850
  60. lemma OAI.HochschildFourPoint.norm_translateB_le line 854
  61. lemma OAI.HochschildFourPoint.translateB_flip_norm line 866
  62. def OAI.HochschildFourPoint.conjugateCLM line 871
  63. lemma OAI.HochschildFourPoint.conjugateCLM_apply line 876
  64. lemma OAI.HochschildFourPoint.conjugateCLM_norm line 880
  65. lemma OAI.HochschildFourPoint.conjugateCLM_nonneg line 886
  66. def OAI.HochschildFourPoint.FunctionalPositive line 891
  67. lemma OAI.HochschildFourPoint.exists_quartic_near line 894
  68. lemma OAI.HochschildFourPoint.exists_quartic_unit line 954
  69. def OAI.HochschildFourPoint.functionalPositiveMap line 1020
  70. theorem OAI.HochschildFourPoint.quartic_state_modulus_unit line 1030
  71. theorem OAI.HochschildFourPoint.quartic_state_modulus line 1061