OAI/MathematicalPhysics/CriticalSK/SpinModel.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CriticalSK.Spin line 26

   Also declared: ComparatorChallenges/CriticalSK.lean:20 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:11 (same declaration text).

2. abbrev OAI.CriticalSK.Edge line 28

   Also declared: ComparatorChallenges/CriticalSK.lean:22 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:13 (same declaration text).

3. abbrev OAI.CriticalSK.Disorder line 30

   Also declared: ComparatorChallenges/CriticalSK.lean:24 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:15 (same declaration text).

4. def OAI.CriticalSK.spinValue line 32

   Also declared: ComparatorChallenges/CriticalSK.lean:26 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:17 (same declaration text).

5. def OAI.CriticalSK.hamiltonian line 34

   Also declared: ComparatorChallenges/CriticalSK.lean:28 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:19 (same declaration text).

6. def OAI.CriticalSK.partition line 37

   Also declared: ComparatorChallenges/CriticalSK.lean:31 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:22 (same declaration text).

7. def OAI.CriticalSK.gibbs line 40

   Also declared: ComparatorChallenges/CriticalSK.lean:34 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:25 (same declaration text).

8. def OAI.CriticalSK.disorderLaw line 43

   Also declared: ComparatorChallenges/CriticalSK.lean:37 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:28 (same declaration text).

9. def OAI.CriticalSK.sameExcept line 46

   Also declared: ComparatorChallenges/CriticalSK.lean:40 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:31 (same declaration text).

10. instance OAI.CriticalSK.(instance at line 49) line 49
11. def OAI.CriticalSK.siteKernel line 52

    Also declared: ComparatorChallenges/CriticalSK.lean:46 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:37 (same declaration text).

12. def OAI.CriticalSK.discreteKernel line 57

    Also declared: ComparatorChallenges/CriticalSK.lean:51 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:42 (same declaration text).

13. def OAI.CriticalSK.generator line 60

    Also declared: ComparatorChallenges/CriticalSK.lean:54 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:45 (same declaration text).

14. def OAI.CriticalSK.continuousKernel line 63

    Also declared: ComparatorChallenges/CriticalSK.lean:57 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:48 (same declaration text).

15. def OAI.CriticalSK.totalVariation line 67

    Also declared: ComparatorChallenges/CriticalSK.lean:61 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:52 (same declaration text).

16. def OAI.CriticalSK.continuousDistance line 70

    Also declared: ComparatorChallenges/CriticalSK.lean:64 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:55 (same declaration text).

17. def OAI.CriticalSK.discreteDistance line 73

    Also declared: ComparatorChallenges/CriticalSK.lean:67 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:58 (same declaration text).

18. def OAI.CriticalSK.continuousMixingTime line 76

    Also declared: ComparatorChallenges/CriticalSK.lean:70 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:61 (same declaration text).

19. def OAI.CriticalSK.discreteMixingTime line 79

    Also declared: ComparatorChallenges/CriticalSK.lean:73 (same declaration text), ComparatorChallenges/CriticalSKMixing.lean:64 (same declaration text).

20. def OAI.CriticalSK.mean line 82

    Also declared: ComparatorChallenges/CriticalSK.lean:76 (same declaration text).

21. def OAI.CriticalSK.variance line 85

    Also declared: ComparatorChallenges/CriticalSK.lean:79 (same declaration text).

22. def OAI.CriticalSK.dirichlet line 88

    Also declared: ComparatorChallenges/CriticalSK.lean:82 (same declaration text).

23. def OAI.CriticalSK.linearObservable line 91

    Also declared: ComparatorChallenges/CriticalSK.lean:85 (same declaration text).

24. def OAI.CriticalSK.covariance line 94

    Also declared: ComparatorChallenges/CriticalSK.lean:88 (same declaration text).

25. def OAI.CriticalSK.covarianceNorm line 99

    Also declared: ComparatorChallenges/CriticalSK.lean:93 (same declaration text).

26. def OAI.CriticalSK.linearRayleigh line 102

    Also declared: ComparatorChallenges/CriticalSK.lean:98 (same declaration text).

27. def OAI.CriticalSK.continuousGoodMass line 106

    Also declared: ComparatorChallenges/CriticalSK.lean:103 (same declaration text).

28. def OAI.CriticalSK.discreteGoodMass line 109

    Distinct definitions of this name: ComparatorChallenges/CriticalSK.lean:107 (same statement text; different proof or body). Qualify references as OAI.CriticalSK.discreteGoodMass@path.

29. lemma OAI.CriticalSK.spinValue_sq line 114
30. def OAI.CriticalSK.cubeVector line 121
31. def OAI.CriticalSK.cubeOverlap line 124
32. instance OAI.CriticalSK.(instance at line 126) line 126
33. instance OAI.CriticalSK.(instance at line 129) line 129
34. def OAI.CriticalSK.gibbsOverlap line 134
35. instance OAI.CriticalSK.(instance at line 139) line 139