OAI/MathematicalPhysics/CriticalSK/PathSpectra.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalSK.edgeTent line 31
  2. lemma OAI.CriticalSK.edgeTent_nonneg line 33
  3. lemma OAI.CriticalSK.edgeTent_le line 35
  4. lemma OAI.CriticalSK.edgeTent_zero_left line 39
  5. lemma OAI.CriticalSK.edgeTent_zero_right line 42
  6. lemma OAI.CriticalSK.edgeTent_plateau line 46
  7. lemma OAI.CriticalSK.edgeTent_lipschitz line 52
  8. lemma OAI.CriticalSK.edgeTent_gradient_support line 61
  9. lemma OAI.CriticalSK.edgeTent_gradient line 68
  10. lemma OAI.CriticalSK.edgeTent_mass line 86
  11. lemma OAI.CriticalSK.edgeCoeff_lower line 105
  12. lemma OAI.CriticalSK.edge_potential_upper line 115
  13. lemma OAI.CriticalSK.edgeTent_energy line 126
  14. lemma OAI.CriticalSK.edgeTent_mul_zero line 150
  15. lemma OAI.CriticalSK.edgeTent_adj_mul_zero line 156
  16. lemma OAI.CriticalSK.edgeTent_adj_mul_zero' line 162
  17. lemma OAI.CriticalSK.separated_tents line 168
  18. lemma OAI.CriticalSK.separated_tents_adj line 177
  19. lemma OAI.CriticalSK.sum_mul_diagonal line 185
  20. def OAI.CriticalSK.tentCombination line 200
  21. lemma OAI.CriticalSK.tentCombination_sq line 203
  22. lemma OAI.CriticalSK.tentCombination_adj line 212
  23. lemma OAI.CriticalSK.tentCombination_mass line 217
  24. lemma OAI.CriticalSK.tentCombination_energy line 223
  25. lemma OAI.CriticalSK.edgeTent_rayleigh line 237
  26. lemma OAI.CriticalSK.tentCombination_rayleigh line 249
  27. lemma OAI.CriticalSK.tentCombination_probe line 270
  28. def OAI.CriticalSK.tentMap line 287
  29. lemma OAI.CriticalSK.tentMap_injective line 298
  30. lemma OAI.CriticalSK.tentMap_rank line 309
  31. lemma OAI.CriticalSK.tentMap_mass line 314
  32. lemma OAI.CriticalSK.eigenvalue_lower_of_subspace line 321
  33. def OAI.CriticalSK.scaledHermite line 349
  34. lemma OAI.CriticalSK.scaledHermite_zero line 353
  35. lemma OAI.CriticalSK.scaledHermite_succ line 355
  36. lemma OAI.CriticalSK.derivative_scaledHermite_succ line 358
  37. lemma OAI.CriticalSK.scaledHermite_three_term line 370
  38. lemma OAI.CriticalSK.scaledHermite_differential line 376
  39. lemma OAI.CriticalSK.scaledHermite_degree_gap line 385
  40. lemma OAI.CriticalSK.scaledHermite_monic line 393
  41. lemma OAI.CriticalSK.scaledHermite_degree line 400
  42. lemma OAI.CriticalSK.det_tridiagonal_step line 409
  43. def OAI.CriticalSK.jacobi line 428
  44. lemma OAI.CriticalSK.jacobi_diagonal line 432
  45. lemma OAI.CriticalSK.jacobi_symmetric line 435
  46. lemma OAI.CriticalSK.jacobi_tail line 440
  47. lemma OAI.CriticalSK.jacobi_row_zero line 447
  48. lemma OAI.CriticalSK.jacobi_col_zero line 450
  49. lemma OAI.CriticalSK.jacobi_first_super line 453
  50. lemma OAI.CriticalSK.jacobi_first_sub line 459
  51. lemma OAI.CriticalSK.charmatrix_jacobi_tail line 465
  52. lemma OAI.CriticalSK.jacobi_charpoly_step line 474
  53. lemma OAI.CriticalSK.jacobi_charpoly line 493
  54. lemma OAI.CriticalSK.finset_sum_indicator_le_one line 502
  55. lemma OAI.CriticalSK.jacobi_row_norm_bound line 513
  56. lemma OAI.CriticalSK.jacobi_hermitian line 534
  57. lemma OAI.CriticalSK.jacobi_eigenvalue_bound line 537
  58. def OAI.CriticalSK.semicircleResolvent line 555
  59. def OAI.CriticalSK.empiricalResolvent line 557
  60. def OAI.CriticalSK.empiricalResolventSquare line 560
  61. lemma OAI.CriticalSK.semicircle_discriminant_pos line 563
  62. lemma OAI.CriticalSK.semicircleResolvent_pos line 565
  63. lemma OAI.CriticalSK.semicircleResolvent_le_one line 571
  64. lemma OAI.CriticalSK.semicircleResolvent_deficit line 577
  65. lemma OAI.CriticalSK.semicircleResolvent_difference line 586
  66. lemma OAI.CriticalSK.semicircle_discriminant_lower line 592
  67. lemma OAI.CriticalSK.empiricalResolvent_pos line 604
  68. lemma OAI.CriticalSK.empiricalResolventSquare_pos line 609
  69. lemma OAI.CriticalSK.empiricalResolvent_le_inv line 615
  70. lemma OAI.CriticalSK.empiricalResolvent_continuousOn line 626
  71. lemma OAI.CriticalSK.empiricalResolvent_hasDerivAt line 635
  72. lemma OAI.CriticalSK.empiricalResolvent_square_difference line 645
  73. lemma OAI.CriticalSK.empiricalResolvent_lt_midpoint line 666
  74. lemma OAI.CriticalSK.empiricalResolvent_lt_semicircle line 692
  75. lemma OAI.CriticalSK.empiricalResolvent_root_difference line 707
  76. lemma OAI.CriticalSK.empiricalResolventSquare_bound line 727
  77. lemma OAI.CriticalSK.empiricalResolvent_error_bound line 761
  78. lemma OAI.CriticalSK.empiricalResolvent_counting line 785
  79. def OAI.CriticalSK.jacobiGaps line 809
  80. lemma OAI.CriticalSK.jacobiGaps_nonneg line 812
  81. lemma OAI.CriticalSK.hermitian_charpoly_derivative_ratio line 816
  82. lemma OAI.CriticalSK.jacobi_charpoly_nonzero line 823
  83. lemma OAI.CriticalSK.jacobi_logarithmic_ratio line 833
  84. lemma OAI.CriticalSK.jacobi_riccati line 850
  85. lemma OAI.CriticalSK.jacobi_resolvent_estimates line 898
  86. lemma OAI.CriticalSK.jacobi_gap_counting line 918
  87. def OAI.CriticalSK.pathOperator line 932
  88. lemma OAI.CriticalSK.pathOperator_symmetric line 935
  89. lemma OAI.CriticalSK.jacobi_edgeCoeff line 938
  90. lemma OAI.CriticalSK.directed_neighbor_sum line 955
  91. lemma OAI.CriticalSK.pathOperator_inner line 975
  92. lemma OAI.CriticalSK.pathOperator_tent_rayleigh line 1001
  93. lemma OAI.CriticalSK.pathOperator_eigenvalue_lower line 1012