OAI/Probability/InvariantIsing/Cavity/CavityRootedResidual.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The quadratic cavity kernel with the common root retained in its state.

  1. def OAI.InvariantIsing.rootedResidualPrior line 13
  2. instance OAI.InvariantIsing.rootedResidualPrior_markov line 20
  3. def OAI.InvariantIsing.rootedResidualWeight line 25
  4. lemma OAI.InvariantIsing.measurable_rootedResidualWeight line 31
  5. lemma OAI.InvariantIsing.measurable_cavityQuadraticResidualGibbs_joint line 42
  6. def OAI.InvariantIsing.cavityRootedResidualBaseKernel line 55
  7. instance OAI.InvariantIsing.cavityRootedResidualBaseKernel_markov line 62
  8. def OAI.InvariantIsing.cavityRootedResidualKernel line 70
  9. instance OAI.InvariantIsing.cavityRootedResidualKernel_markov line 77
  10. def OAI.InvariantIsing.cavityRootedField line 83
  11. lemma OAI.InvariantIsing.measurable_cavityRootedField line 88
  12. lemma OAI.InvariantIsing.cavity_rooted_kernel_test line 93