OAI/Probability/InvariantIsing/Cavity/CavityLabeledModel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The actual finite cavity model in a fixed measurable state space: the tree, Gaussian root and forest are disorder; the leaf, ordinary residual and Ising spin form the configuration.

  1. abbrev OAI.InvariantIsing.CavityLabeledDisorder line 15
  2. abbrev OAI.InvariantIsing.CavityLabeledState line 18
  3. def OAI.InvariantIsing.cavityLabeledDisorderLaw line 21
  4. instance OAI.InvariantIsing.cavityLabeledDisorderLaw_probability line 29
  5. def OAI.InvariantIsing.cavityLabeledLeafKernel line 35
  6. instance OAI.InvariantIsing.cavityLabeledLeafKernel_markov line 38
  7. def OAI.InvariantIsing.cavityLabeledPriorKernel line 41
  8. lemma OAI.InvariantIsing.cavityLabeledPriorKernel_apply line 48
  9. instance OAI.InvariantIsing.cavityLabeledPriorKernel_markov line 56
  10. def OAI.InvariantIsing.cavityLabeledField line 64
  11. lemma OAI.InvariantIsing.measurable_cavityLabeledField line 68
  12. def OAI.InvariantIsing.cavityLabeledEndpoint line 78
  13. lemma OAI.InvariantIsing.measurable_cavityLabeledEndpoint line 83
  14. def OAI.InvariantIsing.cavityLabeledPotential line 97
  15. lemma OAI.InvariantIsing.measurable_cavityLabeledPotential line 103