OAI/Analysis/InterpolatedFactors/GroupBridge.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.FreeFock.semicircular_no_eigenprojection line 22
  2. instance OAI.FreeGroupFactorMain.FreeFock.semicircular_spectral_probability line 87
  3. instance OAI.FreeGroupFactorMain.FreeFock.semicircular_spectral_diffuse line 92
  4. theorem OAI.FreeGroupFactorMain.FreeFock.spectralHaar_mem line 96
  5. def OAI.FreeGroupFactorMain.FreeFock.spectralHaar line 105
  6. theorem OAI.FreeGroupFactorMain.FreeFock.spectralHaar_moment line 113
  7. theorem OAI.FreeGroupFactorMain.lp_strong_limit_of_bounded_basis line 120
  8. theorem OAI.FreeGroupFactorMain.FreeFock.semicircular_mem_haar_bicommutant line 148
  9. def OAI.FreeGroupFactorMain.FreeFock.spectralHaarOperator line 205
  10. theorem OAI.FreeGroupFactorMain.FreeFock.haar_gaussian_commutant line 208
  11. theorem OAI.FreeGroupFactorMain.FreeFock.haar_generated_gaussian line 226
  12. theorem OAI.FreeGroupFactorMain.FreeFock.spectralHaar_cyclic_total line 239
  13. theorem OAI.FreeGroupFactorMain.FreeFock.vacuumTrace_star line 270
  14. theorem OAI.FreeGroupFactorMain.FreeFock.spectralHaar_integer_moment line 275
  15. theorem OAI.FreeGroupFactorMain.FreeFock.wick_replicate_boundary line 291
  16. def OAI.FreeGroupFactorMain.FreeFock.blockLetters line 318
  17. def OAI.FreeGroupFactorMain.FreeFock.blockProduct line 321
  18. def OAI.FreeGroupFactorMain.FreeFock.blocksReduced line 325
  19. theorem OAI.FreeGroupFactorMain.FreeFock.wick_blocks_concatenate line 330
  20. theorem OAI.FreeGroupFactorMain.FreeFock.blockLetters_nonempty line 350
  21. theorem OAI.FreeGroupFactorMain.FreeFock.wick_blocks_centered_moment line 360
  22. theorem OAI.FreeGroupFactorMain.mul_mem_closed_span_image2 line 372
  23. theorem OAI.FreeGroupFactorMain.FreeFock.center_run_mem line 405
  24. theorem OAI.FreeGroupFactorMain.FreeFock.center_run_closure line 423
  25. theorem OAI.FreeGroupFactorMain.FreeFock.spectralHaar_run_closure line 433
  26. theorem OAI.FreeGroupFactorMain.FreeFock.spectralHaar_power_positive_run_closure line 442
  27. def OAI.FreeGroupFactorMain.FreeFock.colorsReduced line 466
  28. def OAI.FreeGroupFactorMain.FreeFock.runProducts line 470
  29. theorem OAI.FreeGroupFactorMain.FreeFock.runProducts_blocks line 474
  30. theorem OAI.FreeGroupFactorMain.FreeFock.blocksReduced_of_colors line 488
  31. theorem OAI.FreeGroupFactorMain.FreeFock.runProducts_trace_zero line 499
  32. theorem OAI.FreeGroupFactorMain.FreeFock.vacuumTrace_span_zero line 510
  33. def OAI.FreeGroupFactorMain.FreeFock.haarProduct line 526
  34. theorem OAI.FreeGroupFactorMain.FreeFock.haarProduct_mem_runProducts line 530
  35. theorem OAI.FreeGroupFactorMain.FreeFock.spectralHaar_mixed_moment line 541
  36. def OAI.FreeGroupFactorMain.adjacentDistinct line 553
  37. def OAI.FreeGroupFactorMain.expandSignedRuns line 557
  38. theorem OAI.FreeGroupFactorMain.reduced_signed_runs line 560
  39. def OAI.FreeGroupFactorMain.signedExponent line 605
  40. theorem OAI.FreeGroupFactorMain.signedExponent_ne_zero line 607
  41. theorem OAI.FreeGroupFactorMain.signedPower line 610
  42. def OAI.FreeGroupFactorMain.signedRunBlocks line 614
  43. theorem OAI.FreeGroupFactorMain.lift_expandSignedRuns line 617
  44. def OAI.FreeGroupFactorMain.FreeFock.haarRepresentation line 633
  45. def OAI.FreeGroupFactorMain.FreeFock.haarOperatorRepresentation line 636
  46. theorem OAI.FreeGroupFactorMain.FreeFock.haarProduct_eq_prod line 640
  47. theorem OAI.FreeGroupFactorMain.FreeFock.haarRepresentation_run_moment line 652
  48. theorem OAI.FreeGroupFactorMain.FreeFock.haarRepresentation_moment line 670
  49. theorem OAI.FreeGroupFactorMain.CyclicUnitary.adjoin_range_span line 698
  50. def OAI.FreeGroupFactorMain.CyclicUnitary.orbitSpan line 722
  51. theorem OAI.FreeGroupFactorMain.CyclicUnitary.apply_mem_orbitSpan line 726
  52. theorem OAI.FreeGroupFactorMain.CyclicUnitary.orbit_inner line 739
  53. def OAI.FreeGroupFactorMain.CyclicUnitary.basis line 748
  54. theorem OAI.FreeGroupFactorMain.CyclicUnitary.basis_inner line 751
  55. theorem OAI.FreeGroupFactorMain.CyclicUnitary.basis_total line 756
  56. def OAI.FreeGroupFactorMain.CyclicUnitary.spatial line 771
  57. theorem OAI.FreeGroupFactorMain.CyclicUnitary.spatial_basis line 778
  58. theorem OAI.FreeGroupFactorMain.FreeFock.haarOperatorRepresentation_star line 787
  59. theorem OAI.FreeGroupFactorMain.FreeFock.haarOperatorRepresentation_of line 794
  60. theorem OAI.FreeGroupFactorMain.FreeFock.haarGroup_cyclic_total line 800
  61. def OAI.FreeGroupFactorMain.FreeFock.haarSpatial line 811
  62. theorem OAI.FreeGroupFactorMain.FreeFock.haarSpatial_basis line 815
  63. theorem OAI.FreeGroupFactorMain.FreeFock.haarSpatial_vacuum line 819
  64. theorem OAI.FreeGroupFactorMain.equiv_mem_centralizer line 830
  65. theorem OAI.FreeGroupFactorMain.equiv_image_centralizer line 845
  66. theorem OAI.FreeGroupFactorMain.equiv_mem_bicommutant line 858
  67. def OAI.FreeGroupFactorMain.restrictStarAlgEquiv line 864
  68. theorem OAI.FreeGroupFactorMain.leftRegular_basis line 879
  69. theorem OAI.FreeGroupFactorMain.FreeFock.haarSpatial_intertwines line 889
  70. theorem OAI.FreeGroupFactorMain.FreeFock.haarRepresentation_commutant line 912
  71. theorem OAI.FreeGroupFactorMain.FreeFock.haarSpatial_mem_vonNeumann line 929
  72. def OAI.FreeGroupFactorMain.FreeFock.gaussianGroupIso line 941
  73. theorem OAI.FreeGroupFactorMain.FreeFock.gaussianGroupIso_trace line 944
  74. def OAI.FreeGroupFactorMain.FreeFock.gaussianUltraweakTopology line 959
  75. theorem OAI.FreeGroupFactorMain.FreeFock.gaussianGroupIso_normal line 964