OAI/Probability/ClassicalON/Model.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ClassicalON.Site line 11

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

2. def OAI.ClassicalON.PositiveNeighbor line 13

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

3. structure OAI.ClassicalON.LatticeGraph line 16

   Also declared: ComparatorChallenges/ClassicalON.lean:16 (same declaration text).

4. abbrev OAI.ClassicalON.Spin line 21

   Also declared: ComparatorChallenges/ClassicalON.lean:21 (same declaration text).

5. abbrev OAI.ClassicalON.Configuration line 22

   Also declared: ComparatorChallenges/ClassicalON.lean:22 (same declaration text).

6. def OAI.ClassicalON.sphereProbability line 24

   Also declared: ComparatorChallenges/ClassicalON.lean:24 (same declaration text).

7. def OAI.ClassicalON.referenceLaw line 28

   Also declared: ComparatorChallenges/ClassicalON.lean:28 (same declaration text).

8. def OAI.ClassicalON.interaction line 31

   Also declared: ComparatorChallenges/ClassicalON.lean:31 (same declaration text).

9. def OAI.ClassicalON.partition line 35

   Also declared: ComparatorChallenges/ClassicalON.lean:35 (same declaration text).

10. def OAI.ClassicalON.correlation line 38

    Also declared: ComparatorChallenges/ClassicalON.lean:38 (same declaration text).

11. def OAI.ClassicalON.siteDistance line 43

    Also declared: ComparatorChallenges/ClassicalON.lean:43 (same declaration text).

12. def OAI.ClassicalON.ExponentialDecay line 46

    Also declared: ComparatorChallenges/ClassicalON.lean:46 (same declaration text).