OAI/Probability/FreeIsing/Model.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.TreeVertex line 11

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

  2. def OAI.Problem367.treeAdj line 14

    Also declared: ComparatorChallenges/FreeIsing.lean:14 (same declaration text).

  3. structure OAI.Problem367.TreeAut line 18

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

  4. def OAI.Problem367.relabel line 22

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

  5. inductive OAI.Problem367.IsingSpin line 26

    Also declared: ComparatorChallenges/FreeIsing.lean:26 (same declaration text).

  6. abbrev OAI.Problem367.IsingSpin.enumList line 31

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

  7. theorem OAI.Problem367.IsingSpin.enumList_getElem?_ctorIdx_eq line 33

    Also declared: ComparatorChallenges/FreeIsing.lean:33 (same declaration text).

  8. theorem OAI.Problem367.IsingSpin.enumList_nodup line 37

    Also declared: ComparatorChallenges/FreeIsing.lean:37 (same declaration text).

  9. instance OAI.Problem367.(instance at line 39) line 39
  10. instance OAI.Problem367.isingSpinMeasurable line 43

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

  11. def OAI.Problem367.uniform01 line 45

    Also declared: ComparatorChallenges/FreeIsing.lean:45 (same declaration text).

  12. instance OAI.Problem367.uniform01Probability line 48

    Also declared: ComparatorChallenges/FreeIsing.lean:48 (same declaration text).

  13. def OAI.Problem367.labelMeasure line 51

    Also declared: ComparatorChallenges/FreeIsing.lean:51 (same declaration text).

  14. def OAI.Problem367.ConnectedFinset line 55

    Also declared: ComparatorChallenges/FreeIsing.lean:55 (same declaration text).

  15. def OAI.Problem367.inducedEdges line 61

    Also declared: ComparatorChallenges/FreeIsing.lean:61 (same declaration text).

  16. def OAI.Problem367.freeCylinderWeight line 67

    Also declared: ComparatorChallenges/FreeIsing.lean:67 (same declaration text).

  17. def OAI.Problem367.HasFreeIsingLaw line 74

    Also declared: ComparatorChallenges/FreeIsing.lean:74 (same declaration text).

  18. def OAI.Problem367.IsFactorOfIID line 80

    Also declared: ComparatorChallenges/FreeIsing.lean:80 (same declaration text).