OAI/MathematicalPhysics/CriticalSK/GaussianMatrices.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalSK.alignIsometry line 23
  2. lemma OAI.CriticalSK.alignIsometry_apply line 27
  3. lemma OAI.CriticalSK.alignIsometry_align line 36
  4. lemma OAI.CriticalSK.alignIsometry_measurable line 41
  5. lemma OAI.CriticalSK.random_isometry_gaussian_preserving line 46
  6. lemma OAI.CriticalSK.exposed_gaussian_alignment line 55
  7. lemma OAI.CriticalSK.covariance_inner_stdGaussian line 60
  8. lemma OAI.CriticalSK.inner_stdGaussian_law line 66
  9. lemma OAI.CriticalSK.gaussian_orthogonal_independent line 76
  10. abbrev OAI.CriticalSK.GaussianMatrix line 88
  11. def OAI.CriticalSK.transposeGaussianMatrix line 91
  12. lemma OAI.CriticalSK.transposeGaussianMatrix_apply line 103
  13. def OAI.CriticalSK.rowIsometry line 106
  14. lemma OAI.CriticalSK.rowIsometry_apply line 110
  15. def OAI.CriticalSK.conjugateGaussianMatrix line 113
  16. lemma OAI.CriticalSK.conjugateGaussianMatrix_preserves line 118
  17. lemma OAI.CriticalSK.euclidean_isometry_apply_eq_sum line 123
  18. lemma OAI.CriticalSK.conjugateGaussianMatrix_apply line 130
  19. lemma OAI.CriticalSK.conjugateGaussianMatrix_transpose line 147
  20. def OAI.CriticalSK.symmetrizeGaussianMatrix line 160
  21. lemma OAI.CriticalSK.symmetrizeGaussianMatrix_continuous line 163
  22. lemma OAI.CriticalSK.conjugate_symmetrize line 168
  23. def OAI.CriticalSK.goeLaw line 175
  24. lemma OAI.CriticalSK.goeLaw_conjugate line 178
  25. lemma OAI.CriticalSK.conjugateGaussianMatrix_measurable line 191
  26. lemma OAI.CriticalSK.random_goe_conjugation_preserving line 215
  27. def OAI.CriticalSK.matrixUnit line 230
  28. lemma OAI.CriticalSK.matrixUnit_inner line 234
  29. lemma OAI.CriticalSK.matrixUnit_apply line 244
  30. def OAI.CriticalSK.goeEntryVector line 250
  31. lemma OAI.CriticalSK.goeEntryVector_inner line 253
  32. lemma OAI.CriticalSK.goe_entry_variance line 257
  33. lemma OAI.CriticalSK.goe_entry_law line 271
  34. abbrev OAI.CriticalSK.UpperEntry line 283
  35. lemma OAI.CriticalSK.goeEntryVector_orthogonal line 285
  36. lemma OAI.CriticalSK.goe_entries_independent line 304
  37. def OAI.CriticalSK.upperRead line 334
  38. def OAI.CriticalSK.upperWrite line 336
  39. lemma OAI.CriticalSK.upperRead_measurable line 340
  40. lemma OAI.CriticalSK.upperWrite_measurable line 345
  41. lemma OAI.CriticalSK.upperWrite_upperRead line 355
  42. lemma OAI.CriticalSK.upperRead_upperWrite line 363
  43. lemma OAI.CriticalSK.goe_symmetric_ae line 368
  44. lemma OAI.CriticalSK.goe_upper_law line 376
  45. lemma OAI.CriticalSK.goeLaw_eq_upper_product line 385
  46. def OAI.CriticalSK.upperSplit line 397
  47. lemma OAI.CriticalSK.upperSplit_diag line 420
  48. lemma OAI.CriticalSK.upperSplit_column line 422
  49. lemma OAI.CriticalSK.upperSplit_tail line 425
  50. def OAI.CriticalSK.goeUpperMarginal line 429
  51. instance OAI.CriticalSK.goeUpperMarginal_probability line 432
  52. def OAI.CriticalSK.splitUpper line 437
  53. lemma OAI.CriticalSK.splitUpper_preserving line 442
  54. def OAI.CriticalSK.extendTailIsometry line 461
  55. lemma OAI.CriticalSK.extendTailIsometry_zero line 498
  56. lemma OAI.CriticalSK.extendTailIsometry_succ line 502
  57. lemma OAI.CriticalSK.extendTailIsometry_basis_zero line 507
  58. lemma OAI.CriticalSK.extendTailIsometry_basis_succ line 521
  59. def OAI.CriticalSK.borderMatrix line 534
  60. lemma OAI.CriticalSK.borderMatrix_zero_zero line 539
  61. lemma OAI.CriticalSK.borderMatrix_zero_succ line 542
  62. lemma OAI.CriticalSK.borderMatrix_succ_zero line 545
  63. lemma OAI.CriticalSK.borderMatrix_succ_succ line 548
  64. lemma OAI.CriticalSK.extendTailIsometry_border line 551
  65. instance OAI.CriticalSK.goeLaw_probability line 574
  66. def OAI.CriticalSK.matrixTail line 579
  67. def OAI.CriticalSK.goeBlocks line 582
  68. lemma OAI.CriticalSK.matrixTail_measurable line 586
  69. lemma OAI.CriticalSK.goeBlocks_measurable line 595
  70. lemma OAI.CriticalSK.borderMatrix_blocks line 599
  71. lemma OAI.CriticalSK.goeBlocks_preserving line 609
  72. lemma OAI.CriticalSK.aligned_goeBlock_preserving line 632
  73. lemma OAI.CriticalSK.exposed_column_tail_law line 646
  74. lemma OAI.CriticalSK.goe_step_conjugate line 657
  75. def OAI.CriticalSK.orthoMatrix line 677
  76. def OAI.CriticalSK.matrixOfGaussian line 680
  77. lemma OAI.CriticalSK.matrixOfGaussian_injective line 682
  78. lemma OAI.CriticalSK.orthoMatrix_trans line 687
  79. lemma OAI.CriticalSK.matrixOfGaussian_conjugate line 697
  80. lemma OAI.CriticalSK.conjugateGaussianMatrix_trans line 706
  81. lemma OAI.CriticalSK.conjugate_symmetric line 714
  82. def OAI.CriticalSK.firstAxis line 727
  83. lemma OAI.CriticalSK.firstAxis_succ line 730
  84. lemma OAI.CriticalSK.firstAxis_norm_succ line 734
  85. lemma OAI.CriticalSK.align_firstAxis line 738
  86. lemma OAI.CriticalSK.extendTailIsometry_firstAxis line 744
  87. def OAI.CriticalSK.firstColumn line 750
  88. def OAI.CriticalSK.reducedTail line 753
  89. lemma OAI.CriticalSK.reducedTail_symmetric line 756
  90. lemma OAI.CriticalSK.firstColumn_measurable line 760
  91. lemma OAI.CriticalSK.reducedTail_measurable line 766
  92. lemma OAI.CriticalSK.first_step_conjugate line 772
  93. def OAI.CriticalSK.triReduce line 783
  94. def OAI.CriticalSK.triIsometry line 787
  95. lemma OAI.CriticalSK.triIsometry_firstAxis line 793
  96. lemma OAI.CriticalSK.triReduce_conjugate line 799
  97. lemma OAI.CriticalSK.borderMatrix_measurable line 811
  98. lemma OAI.CriticalSK.triReduce_measurable line 827
  99. def OAI.CriticalSK.columnNormLaw line 836
  100. def OAI.CriticalSK.assembleTri line 840
  101. lemma OAI.CriticalSK.assembleTri_measurable line 843
  102. def OAI.CriticalSK.triMatrixLaw line 848
  103. lemma OAI.CriticalSK.columnNorm_preserving line 853
  104. instance OAI.CriticalSK.columnNormLaw_probability line 858
  105. instance OAI.CriticalSK.triMatrixLaw_probability line 862
  106. lemma OAI.CriticalSK.triReduce_preserving line 869