OAI/MathematicalPhysics/CriticalSK/DisorderTransfer.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.symmetric_sum_upper line 75
  2. def OAI.CriticalSK.matrixDisorder line 106
  3. def OAI.CriticalSK.matrixEnergy line 108
  4. lemma OAI.CriticalSK.matrixEnergy_hamiltonian line 111
  5. lemma OAI.CriticalSK.matrixEnergy_inner line 123
  6. def OAI.CriticalSK.matrixGibbs line 136
  7. lemma OAI.CriticalSK.matrixGibbs_eq line 139
  8. lemma OAI.CriticalSK.gibbs_continuous line 145
  9. def OAI.CriticalSK.linearSmallBall line 151
  10. lemma OAI.CriticalSK.linearSmallBall_nonneg line 154
  11. lemma OAI.CriticalSK.linearSmallBall_le_one line 159
  12. lemma OAI.CriticalSK.linearSmallBall_continuous line 166
  13. def OAI.CriticalSK.smallBallObstruction line 175
  14. lemma OAI.CriticalSK.smallBallObstruction_closed line 178
  15. lemma OAI.CriticalSK.linearObservable_inner line 187
  16. def OAI.CriticalSK.rotatedDirection line 195
  17. lemma OAI.CriticalSK.rotatedDirection_norm line 198
  18. lemma OAI.CriticalSK.rotatedDirection_observable line 203
  19. lemma OAI.CriticalSK.gibbs_exp_shift line 208
  20. lemma OAI.CriticalSK.rotatedCubeSmallBall_eq line 214
  21. lemma OAI.CriticalSK.smallBallObstruction_rotation line 228
  22. lemma OAI.CriticalSK.orthogonalIsometry_one line 236
  23. lemma OAI.CriticalSK.orthogonalIsometry_inv line 239
  24. lemma OAI.CriticalSK.continuous_pair_transform line 246
  25. lemma OAI.CriticalSK.orthogonalIsometry_symm_continuous line 251
  26. def OAI.CriticalSK.haarConjugate line 261
  27. lemma OAI.CriticalSK.haarConjugate_measurable line 264
  28. lemma OAI.CriticalSK.gaussian_matrix_energy_eigenbasis line 272
  29. lemma OAI.CriticalSK.haarConjugate_energy line 283
  30. lemma OAI.CriticalSK.haarConjugate_hamiltonian line 296
  31. lemma OAI.CriticalSK.goe_haar_preserving line 312
  32. lemma OAI.CriticalSK.preserving_product_event_real line 318
  33. lemma OAI.CriticalSK.goe_haar_event_identity line 342
  34. def OAI.CriticalSK.gaussianDisorder line 349
  35. lemma OAI.CriticalSK.gaussianDisorder_measurable line 352
  36. lemma OAI.CriticalSK.goe_disorder_law line 358
  37. lemma OAI.CriticalSK.haar_smallBallObstruction_bound line 381
  38. lemma OAI.CriticalSK.goe_event_from_orbit_bound line 408