OAI/Probability/InvariantIsing/Cavity/CavityBaseRestrictedLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The restricted base/cavity test in the exact product coordinates: the shared cascade leaf stays with the base Gibbs law.

  1. def OAI.InvariantIsing.cavityPairLeafSwap line 16
  2. def OAI.InvariantIsing.cavityPairLeafUnswap line 20
  3. lemma OAI.InvariantIsing.cavity_pair_leaf_swap_preserving line 24
  4. theorem OAI.InvariantIsing.cavity_base_restricted_product line 39