OAI/Analysis/InterpolatedFactors/Haar.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeGroupFactorMain.CyclicSpectral.Space line 18
  2. instance OAI.FreeGroupFactorMain.CyclicSpectral.compactSpace line 20
  3. def OAI.FreeGroupFactorMain.CyclicSpectral.functional line 22
  4. def OAI.FreeGroupFactorMain.CyclicSpectral.measure line 41
  5. instance OAI.FreeGroupFactorMain.CyclicSpectral.measure_regular line 43
  6. instance OAI.FreeGroupFactorMain.CyclicSpectral.measure_finite line 46
  7. theorem OAI.FreeGroupFactorMain.CyclicSpectral.integral_continuous line 48
  8. theorem OAI.FreeGroupFactorMain.CyclicSpectral.measure_univ line 53
  9. theorem OAI.FreeGroupFactorMain.CyclicSpectral.integral_sq line 60
  10. theorem OAI.FreeGroupFactorMain.CyclicSpectral.probability line 77
  11. def OAI.FreeGroupFactorMain.CyclicSpectral.complexHom line 87
  12. def OAI.FreeGroupFactorMain.CyclicSpectral.complexLift line 91
  13. theorem OAI.FreeGroupFactorMain.CyclicSpectral.complexHom_real line 94
  14. theorem OAI.FreeGroupFactorMain.CyclicSpectral.real_inner_im line 99
  15. theorem OAI.FreeGroupFactorMain.CyclicSpectral.integral_complexLift line 113
  16. theorem OAI.FreeGroupFactorMain.CyclicSpectral.integral_complex line 122
  17. theorem OAI.FreeGroupFactorMain.CyclicSpectral.complexHom_mem line 143
  18. def OAI.FreeGroupFactorMain.CyclicSpectral.complexEvaluate line 153
  19. theorem OAI.FreeGroupFactorMain.CyclicSpectral.complexEvaluate_inner line 156
  20. theorem OAI.FreeGroupFactorMain.CyclicSpectral.complexEvaluate_norm line 171
  21. def OAI.FreeGroupFactorMain.CyclicSpectral.complexRealize line 182
  22. theorem OAI.FreeGroupFactorMain.CyclicSpectral.complexRealize_continuous line 185
  23. theorem OAI.FreeGroupFactorMain.CyclicSpectral.complexRealize_norm line 193
  24. def OAI.FreeGroupFactorMain.CyclicSpectral.complexIsometry line 201
  25. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.continuous_cdf line 213
  26. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.level_greatest line 223
  27. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.measure_cdf_sublevel line 248
  28. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.measure_cdf_zero line 254
  29. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.map_cdf line 268
  30. def OAI.FreeGroupFactorMain.ProbabilityTransform.phase line 302
  31. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.phase_continuous line 304
  32. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.phase_star_mul line 307
  33. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.phase_uniform_moment line 315
  34. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.phase_cdf_moment line 335
  35. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.measure_cdf_le line 347
  36. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.cdf_cut_ae line 360
  37. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.cdf_injective_conull line 370
  38. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.cdf_between_ae line 390
  39. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.phase_injectiveOn line 403
  40. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.phase_cdf_injective_conull line 419
  41. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.exists_measurable_phase_inverse line 433
  42. def OAI.FreeGroupFactorMain.ProbabilityTransform.haarMeasure line 466
  43. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.haarTransform_measurable line 468
  44. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.haarTransform_preserving line 471
  45. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.haarPullback_surjective line 475
  46. def OAI.FreeGroupFactorMain.ProbabilityTransform.haarL2Equiv line 494
  47. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.haarL2Equiv_apply line 499
  48. instance OAI.FreeGroupFactorMain.ProbabilityTransform.haarMeasure_probability line 503
  49. theorem OAI.FreeGroupFactorMain.ProbabilityTransform.haar_boundedContinuous_dense line 507
  50. theorem OAI.FreeGroupFactorMain.SpectralPullback.pullback_surjective line 520
  51. def OAI.FreeGroupFactorMain.SpectralPullback.equivalence line 537
  52. theorem OAI.FreeGroupFactorMain.SpectralPullback.equivalence_apply line 541
  53. def OAI.FreeGroupFactorMain.CyclicSpectral.realMeasure line 552
  54. instance OAI.FreeGroupFactorMain.CyclicSpectral.realMeasure_probability line 554
  55. instance OAI.FreeGroupFactorMain.CyclicSpectral.realMeasure_noAtoms line 558
  56. def OAI.FreeGroupFactorMain.CyclicSpectral.haarFunction line 576
  57. theorem OAI.FreeGroupFactorMain.CyclicSpectral.haarFunction_unitary line 581
  58. def OAI.FreeGroupFactorMain.CyclicSpectral.haarUnitary line 592
  59. theorem OAI.FreeGroupFactorMain.CyclicSpectral.haarUnitary_moment line 595
  60. def OAI.FreeGroupFactorMain.CyclicSpectral.realL2Equiv line 612
  61. theorem OAI.FreeGroupFactorMain.CyclicSpectral.realL2Equiv_apply line 618
  62. def OAI.FreeGroupFactorMain.CyclicSpectral.haarSpectralTransfer line 622
  63. theorem OAI.FreeGroupFactorMain.CyclicSpectral.haarSpectralTransfer_continuous line 627
  64. theorem OAI.FreeGroupFactorMain.CyclicSpectral.haar_spectral_functions_dense line 645
  65. theorem OAI.FreeGroupFactorMain.CyclicSpectral.haar_cyclic_contains_continuous line 663
  66. theorem OAI.FreeGroupFactorMain.CyclicSpectral.haar_cyclic_contains_operator line 678
  67. theorem OAI.FreeGroupFactorMain.CyclicSpectral.complexHom_continuous line 690
  68. theorem OAI.FreeGroupFactorMain.CyclicSpectral.complexHom_composition line 694
  69. theorem OAI.FreeGroupFactorMain.CyclicSpectral.complexHom_composition_mem line 706
  70. def OAI.FreeGroupFactorMain.CyclicSpectral.scalarClip line 717
  71. theorem OAI.FreeGroupFactorMain.CyclicSpectral.continuous_scalarClip line 718
  72. theorem OAI.FreeGroupFactorMain.CyclicSpectral.norm_scalarClip line 721
  73. theorem OAI.FreeGroupFactorMain.CyclicSpectral.scalarClip_error line 724
  74. def OAI.FreeGroupFactorMain.CyclicSpectral.clipFunction line 745
  75. theorem OAI.FreeGroupFactorMain.CyclicSpectral.clipFunction_norm line 747
  76. def OAI.FreeGroupFactorMain.CyclicSpectral.coordinate line 759
  77. theorem OAI.FreeGroupFactorMain.CyclicSpectral.complexHom_coordinate line 761
  78. theorem OAI.FreeGroupFactorMain.CyclicSpectral.clip_vector_error line 765
  79. theorem OAI.FreeGroupFactorMain.CyclicSpectral.bounded_haar_approx line 785
  80. theorem OAI.FreeGroupFactorMain.strong_limit_of_bounded_total line 803
  81. theorem OAI.FreeGroupFactorMain.CyclicSpectral.operator_mem_haar_bicommutant line 838