OAI/MathematicalPhysics/PlanarAnderson/Spectrum.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

The nearest-neighbor Anderson operator on the square lattice and its almost-sure spectral interval.

  1. abbrev OAI.PlanarAnderson.Site line 12

    Also declared: ComparatorChallenges/PlanarAndersonSpectrum.lean:11 (same declaration text).

  2. abbrev OAI.PlanarAnderson.Configuration line 13

    Also declared: ComparatorChallenges/PlanarAndersonSpectrum.lean:12 (same declaration text).

  3. abbrev OAI.PlanarAnderson.Hilbert line 14

    Also declared: ComparatorChallenges/PlanarAndersonSpectrum.lean:13 (same declaration text).

  4. instance OAI.PlanarAnderson.(instance at line 16) line 16
  5. def OAI.PlanarAnderson.disorderLaw line 22

    Also declared: ComparatorChallenges/PlanarAndersonSpectrum.lean:15 (same declaration text).

  6. def OAI.PlanarAnderson.IsAndersonOperator line 25

    Also declared: ComparatorChallenges/PlanarAndersonSpectrum.lean:18 (same declaration text).

  7. def OAI.PlanarAnderson.spectralInterval line 30

    Also declared: ComparatorChallenges/PlanarAndersonSpectrum.lean:23 (same declaration text).

  8. def OAI.PlanarAnderson.eigenvalues line 33
  9. def OAI.PlanarAnderson.PurePoint line 36
  10. def OAI.PlanarAnderson.HasCompleteOrthonormalEigenbasis line 39
  11. def OAI.PlanarAnderson.MainStatement line 42
  12. theorem OAI.PlanarAnderson.mem_reindex line 47
  13. def OAI.PlanarAnderson.permute line 52
  14. theorem OAI.PlanarAnderson.permute_apply line 61
  15. def OAI.PlanarAnderson.translation line 64
  16. theorem OAI.PlanarAnderson.translation_apply line 70
  17. theorem OAI.PlanarAnderson.inner_permute line 72
  18. def OAI.PlanarAnderson.hopping line 78
  19. theorem OAI.PlanarAnderson.hopping_apply line 84
  20. theorem OAI.PlanarAnderson.norm_hopping_le line 89
  21. theorem OAI.PlanarAnderson.translation_symm line 107
  22. theorem OAI.PlanarAnderson.hopping_selfAdjoint line 113
  23. def OAI.PlanarAnderson.potential line 122
  24. theorem OAI.PlanarAnderson.potential_apply line 128
  25. theorem OAI.PlanarAnderson.norm_potential_le line 132
  26. theorem OAI.PlanarAnderson.potential_selfAdjoint line 136
  27. def OAI.PlanarAnderson.anderson line 146
  28. theorem OAI.PlanarAnderson.anderson_formula line 149
  29. theorem OAI.PlanarAnderson.anderson_selfAdjoint line 154
  30. theorem OAI.PlanarAnderson.norm_anderson_le line 160
  31. theorem OAI.PlanarAnderson.anderson_unique line 164
  32. theorem OAI.PlanarAnderson.spectrum_subset line 169
  33. theorem OAI.PlanarAnderson.uniform_probability line 179
  34. theorem OAI.PlanarAnderson.bounded_ae line 187
  35. theorem OAI.PlanarAnderson.anderson_exists_ae line 197
  36. def OAI.PlanarAnderson.cube line 205
  37. def OAI.PlanarAnderson.outerCube line 206
  38. def OAI.PlanarAnderson.innerCube line 208
  39. def OAI.PlanarAnderson.boundary line 210
  40. def OAI.PlanarAnderson.plane line 212
  41. def OAI.PlanarAnderson.cutWave line 213
  42. def OAI.PlanarAnderson.freeEnergy line 215
  43. theorem OAI.PlanarAnderson.cutWave_apply line 217
  44. theorem OAI.PlanarAnderson.plane_norm line 222
  45. theorem OAI.PlanarAnderson.cube_card line 225
  46. theorem OAI.PlanarAnderson.cutWave_norm line 228
  47. theorem OAI.PlanarAnderson.cutWave_point_bound line 239
  48. theorem OAI.PlanarAnderson.freeEnergy_norm_le line 244
  49. theorem OAI.PlanarAnderson.plane_hopping line 251
  50. theorem OAI.PlanarAnderson.free_error_inner line 261
  51. theorem OAI.PlanarAnderson.free_error_outer line 275
  52. theorem OAI.PlanarAnderson.boundary_card line 288
  53. theorem OAI.PlanarAnderson.free_error_point_bound line 309
  54. theorem OAI.PlanarAnderson.finite_norm_sq line 325
  55. theorem OAI.PlanarAnderson.free_error_norm_sq line 334
  56. theorem OAI.PlanarAnderson.free_error_relative line 352
  57. theorem OAI.PlanarAnderson.diagonal_error_bound line 370
  58. theorem OAI.PlanarAnderson.anderson_shift line 397
  59. theorem OAI.PlanarAnderson.constant_box_relative line 406
  60. theorem OAI.PlanarAnderson.spectrum_of_approximate line 432
  61. theorem OAI.PlanarAnderson.freeEnergy_surjective line 460
  62. theorem OAI.PlanarAnderson.iid_exists_ae line 476
  63. abbrev OAI.PlanarAnderson.Patch line 497
  64. def OAI.PlanarAnderson.patchSite line 499
  65. def OAI.PlanarAnderson.trialSite line 500
  66. theorem OAI.PlanarAnderson.trialSite_injective line 503
  67. theorem OAI.PlanarAnderson.trial_law line 526
  68. theorem OAI.PlanarAnderson.uniform_interval_pos line 540
  69. theorem OAI.PlanarAnderson.constant_trial_ae line 555
  70. def OAI.PlanarAnderson.HasConstantBoxes line 578
  71. theorem OAI.PlanarAnderson.constant_boxes_ae line 582
  72. theorem OAI.PlanarAnderson.cube_is_patch line 615
  73. theorem OAI.PlanarAnderson.spectrum_contains_shifted_free line 621
  74. theorem OAI.PlanarAnderson.spectrum_contains_interior line 637
  75. theorem OAI.PlanarAnderson.spectrum_eq_interval line 659
  76. theorem OAI.PlanarAnderson.anderson_spectrum_ae line 674

    Distinct definitions of this name: ComparatorChallenges/PlanarAndersonSpectrum.lean:26 (same statement text; different proof or body). Qualify references as OAI.PlanarAnderson.anderson_spectrum_ae@path.

  77. theorem OAI.PlanarAnderson.purePoint_of_completeOrthonormalEigenbasis line 681
  78. theorem OAI.PlanarAnderson.eigenvalues_subset_spectrum line 692
  79. theorem OAI.PlanarAnderson.closure_eigenvalues_subset_spectrum line 701
  80. theorem OAI.PlanarAnderson.spectrum_eq_closure_eigenvalues_of_completeOrthonormalEigenbasis line 705