OAI/Probability/InvariantIsing/Cavity/CavityFiniteExponentLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A depth-n cascade only uses its first n exponents. This identifies the uniform approximation convention with the field-chain convention.

  1. lemma OAI.InvariantIsing.cavity_labeled_exponent_congr line 13
  2. lemma OAI.InvariantIsing.cavity_cascade_exponent_congr line 31
  3. lemma OAI.InvariantIsing.cavity_uniform_chain_exponent line 37
  4. lemma OAI.InvariantIsing.cavity_uniform_chain_law line 42