OAI/MathematicalPhysics/Anderson/Certificates.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

Uniform-site Anderson operators and measurable finite-volume certificate events.

  1. abbrev OAI.Anderson.Site line 14
  2. abbrev OAI.Anderson.SingleSite line 16
  3. instance OAI.Anderson.singleSiteMeasureSpace line 18
  4. def OAI.Anderson.uniformSite line 20
  5. instance OAI.Anderson.uniformSite_isProbabilityMeasure line 22
  6. lemma OAI.Anderson.uniformSite_map_val line 29
  7. abbrev OAI.Anderson.Configuration line 36
  8. def OAI.Anderson.disorderLaw line 38
  9. instance OAI.Anderson.disorderLaw_isProbabilityMeasure line 41
  10. def OAI.Anderson.potential line 46
  11. lemma OAI.Anderson.potential_mem_Icc line 48
  12. lemma OAI.Anderson.abs_potential_le_one line 51
  13. lemma OAI.Anderson.site_marginal line 54
  14. lemma OAI.Anderson.potential_measurable line 58
  15. lemma OAI.Anderson.potential_distribution line 62
  16. lemma OAI.Anderson.cylinder_probability line 69
  17. abbrev OAI.Anderson.StateSpace line 74
  18. def OAI.Anderson.reindexL2 line 76
  19. def OAI.Anderson.shift line 93
  20. lemma OAI.Anderson.shift_apply line 96
  21. lemma OAI.Anderson.shift_norm line 99
  22. lemma OAI.Anderson.norm_shift_le_one line 102
  23. lemma OAI.Anderson.inner_shift line 107
  24. def OAI.Anderson.basisVector line 113
  25. def OAI.Anderson.hopping line 115
  26. lemma OAI.Anderson.shift_pair_isSelfAdjoint line 118
  27. lemma OAI.Anderson.hopping_isSelfAdjoint line 127
  28. def OAI.Anderson.potentialLinear line 132
  29. lemma OAI.Anderson.potentialLinear_norm_le line 143
  30. def OAI.Anderson.potentialOperator line 151
  31. lemma OAI.Anderson.potentialOperator_apply line 156
  32. lemma OAI.Anderson.norm_potentialOperator_le_one line 160
  33. lemma OAI.Anderson.potentialOperator_isSelfAdjoint line 167
  34. def OAI.Anderson.hamiltonian line 178
  35. lemma OAI.Anderson.hamiltonian_isSelfAdjoint line 182
  36. lemma OAI.Anderson.hamiltonian_apply line 189
  37. lemma OAI.Anderson.norm_hopping_le line 199
  38. lemma OAI.Anderson.norm_hamiltonian_le line 214
  39. def OAI.Anderson.higherDimWindow line 224
  40. def OAI.Anderson.energyWindow line 227
  41. lemma OAI.Anderson.energyWindow_three line 230
  42. lemma OAI.Anderson.energyWindow_of_four_le line 234
  43. lemma OAI.Anderson.energyWindow_open line 238
  44. lemma OAI.Anderson.energyWindow_nonempty line 242
  45. lemma OAI.Anderson.energyWindow_subset_freeBand line 249
  46. def OAI.Anderson.sideLength line 263
  47. instance OAI.Anderson.sideLength_neZero line 265
  48. abbrev OAI.Anderson.Torus line 268
  49. abbrev OAI.Anderson.TorusConfiguration line 270
  50. def OAI.Anderson.torusLaw line 272
  51. instance OAI.Anderson.torusLaw_isProbabilityMeasure line 275
  52. lemma OAI.Anderson.torus_card line 279
  53. def OAI.Anderson.torusBasisVector line 282
  54. def OAI.Anderson.periodicHamiltonian line 284
  55. def OAI.Anderson.diagonalOn line 291
  56. def OAI.Anderson.scaleCoupling line 295
  57. def OAI.Anderson.scaleHeight line 297
  58. def OAI.Anderson.certificateMatrix line 299
  59. def OAI.Anderson.certificateEvent line 305
  60. lemma OAI.Anderson.continuous_periodicHamiltonian line 314
  61. lemma OAI.Anderson.continuous_diagonalOn line 322
  62. lemma OAI.Anderson.certificateEvent_measurableSet line 330
  63. def OAI.Anderson.thresholdCriterion line 393
  64. lemma OAI.Anderson.certificateEvent_mono line 399
  65. lemma OAI.Anderson.thresholdCriterion_mono line 410
  66. def OAI.Anderson.finiteBoxThreshold line 418
  67. lemma OAI.Anderson.finiteBoxThreshold_exists_iff line 422
  68. lemma OAI.Anderson.thresholdIndex_unique line 432
  69. lemma OAI.Anderson.finiteBoxThreshold_unique line 437
  70. lemma OAI.Anderson.finiteBoxThreshold_pos line 443
  71. lemma OAI.Anderson.coupling_parametrization line 447
  72. structure OAI.Anderson.SpectralResolution line 492
  73. def OAI.Anderson.SpectralResolution.acVectors line 515
  74. lemma OAI.Anderson.SpectralResolution.mem_acVectors_iff line 517
  75. def OAI.Anderson.SpectralResolution.acSubspace line 531
  76. lemma OAI.Anderson.SpectralResolution.mem_acSubspace line 546
  77. lemma OAI.Anderson.SpectralResolution.isClosed_acVectors line 549
  78. def OAI.Anderson.SpectralResolution.purelyACOn line 563
  79. lemma OAI.Anderson.SpectralResolution.projection_idempotent line 566
  80. lemma OAI.Anderson.SpectralResolution.vectorMeasure_univ line 570
  81. lemma OAI.Anderson.SpectralResolution.vectorMeasure_projection line 575
  82. lemma OAI.Anderson.SpectralResolution.range_subset_acVectors_iff line 582