OAI/Probability/InvariantIsing/Cavity/CavityFullGibbs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A total probability-kernel version of the full cavity Gibbs law. Its fallback on a nonintegrable fiber is irrelevant on the proved full-measure set.

  1. def OAI.InvariantIsing.cavityRootedFullGibbs line 15
  2. instance OAI.InvariantIsing.cavityRootedFullGibbs_markov line 35
  3. theorem OAI.InvariantIsing.cavityRootedFullGibbs_eq_tilted line 43