OAI/MathematicalPhysics/CriticalSK/GOESpectrum.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.symmetric_eigenvalue_norm_bound line 29
  2. def OAI.CriticalSK.gaussianMatrixCLM line 44
  3. def OAI.CriticalSK.gaussianMatrixToCLM line 48
  4. lemma OAI.CriticalSK.finite_real_linear_continuous line 60
  5. lemma OAI.CriticalSK.gaussianMatrixCLM_continuous line 64
  6. lemma OAI.CriticalSK.gaussianMatrixCLM_symmetric line 68
  7. lemma OAI.CriticalSK.symmetrize_half_entry line 74
  8. lemma OAI.CriticalSK.symmetrize_half_symmetric line 79
  9. lemma OAI.CriticalSK.symmetrize_half_eq line 84
  10. def OAI.CriticalSK.matrixOrderedEigenvalues line 90
  11. lemma OAI.CriticalSK.matrixOrderedEigenvalues_eq line 93
  12. lemma OAI.CriticalSK.matrixOrderedEigenvalues_continuous line 100
  13. lemma OAI.CriticalSK.orthoMatrix_transpose line 116
  14. lemma OAI.CriticalSK.orthoMatrix_toLpLin line 125
  15. lemma OAI.CriticalSK.gaussianMatrixCLM_conjugate line 135
  16. lemma OAI.CriticalSK.matrixOrderedEigenvalues_conjugate line 145
  17. lemma OAI.CriticalSK.matrixOrderedEigenvalues_triReduce line 153
  18. lemma OAI.CriticalSK.matrixOrderedEigenvalues_sample line 159
  19. def OAI.CriticalSK.triEntriesLaw line 169
  20. instance OAI.CriticalSK.triEntriesLaw_probability line 172
  21. def OAI.CriticalSK.triEntriesMatrix line 175
  22. lemma OAI.CriticalSK.triEntriesMatrix_measurable line 179
  23. lemma OAI.CriticalSK.triEntriesLaw_split line 188
  24. lemma OAI.CriticalSK.probability_eq_on_subsingleton line 199
  25. lemma OAI.CriticalSK.triEntriesMatrix_preserving line 209
  26. lemma OAI.CriticalSK.triEntriesMatrix_apply line 224
  27. def OAI.CriticalSK.goeScale line 257
  28. lemma OAI.CriticalSK.goeScale_square line 259
  29. lemma OAI.CriticalSK.goeScale_diagonal line 265
  30. lemma OAI.CriticalSK.gaussian_div_sqrt_preserving line 270
  31. lemma OAI.CriticalSK.chi_eq_norm line 280
  32. lemma OAI.CriticalSK.columnNormLaw_scale line 285
  33. lemma OAI.CriticalSK.columnNormLaw_zero line 305
  34. lemma OAI.CriticalSK.measurePreserving_independent line 312
  35. lemma OAI.CriticalSK.diagonalMarginal_scale line 322
  36. lemma OAI.CriticalSK.diagonalFinite_preserving line 331
  37. def OAI.CriticalSK.finiteChiEntry line 340
  38. lemma OAI.CriticalSK.finiteChiEntry_measurable line 343
  39. lemma OAI.CriticalSK.finiteChiEntry_preserving line 349
  40. lemma OAI.CriticalSK.chiFinite_preserving line 362
  41. def OAI.CriticalSK.sampleEntries line 372
  42. lemma OAI.CriticalSK.sampleEntries_preserving line 375
  43. lemma OAI.CriticalSK.sampleEntriesMatrix_apply line 390
  44. lemma OAI.CriticalSK.sampleMatrix_preserving line 405
  45. lemma OAI.CriticalSK.matrixOrderedEigenvalues_measurable line 415
  46. lemma OAI.CriticalSK.goe_sample_eigenvalues_law line 419
  47. def OAI.CriticalSK.spectralGood line 435
  48. lemma OAI.CriticalSK.spectralGood_measurable line 439
  49. lemma OAI.CriticalSK.sampleEigenvalues_measurable line 445
  50. lemma OAI.CriticalSK.goe_spectral_bad_probability line 449