OAI/Probability/FreeIsing/Trees/ClusterInputSampler.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.ClusterInput.Rows line 16
  2. abbrev OAI.Problem367.ClusterInput.Space line 18
  3. def OAI.Problem367.ClusterInput.rowLaw line 21
  4. def OAI.Problem367.ClusterInput.law line 24
  5. instance OAI.Problem367.ClusterInput.rowLaw_probability line 27
  6. instance OAI.Problem367.ClusterInput.law_probability line 31
  7. def OAI.Problem367.ClusterInput.relabelRows line 35
  8. def OAI.Problem367.ClusterInput.relabelInputs line 38
  9. abbrev OAI.Problem367.ClusterInput.Seed line 41
  10. def OAI.Problem367.ClusterInput.seedLaw line 43
  11. instance OAI.Problem367.ClusterInput.seedLaw_probability line 46
  12. def OAI.Problem367.ClusterInput.unpack line 50
  13. lemma OAI.Problem367.ClusterInput.measurable_unpack line 53
  14. lemma OAI.Problem367.ClusterInput.unpack_relabel line 57
  15. lemma OAI.Problem367.ClusterInput.map_flatten_rows line 60
  16. lemma OAI.Problem367.ClusterInput.map_unpack line 66
  17. theorem OAI.Problem367.ClusterInput.exists_sampler line 98
  18. abbrev OAI.Problem367.ClusterInput.SpinSpace line 111
  19. def OAI.Problem367.ClusterInput.spinLaw line 114
  20. def OAI.Problem367.ClusterInput.relabelSpinInputs line 118
  21. def OAI.Problem367.ClusterInput.toSpinInputs line 121
  22. lemma OAI.Problem367.ClusterInput.measurable_toSpinInputs line 124
  23. lemma OAI.Problem367.ClusterInput.toSpinInputs_relabel line 129
  24. lemma OAI.Problem367.ClusterInput.map_toSpinInputs line 132
  25. theorem OAI.Problem367.ClusterInput.exists_spin_sampler line 143
  26. theorem OAI.Problem367.ClusterInput.isFactorOfIID_of_spin_inputs line 155