OAI/Probability/InvariantIsing/Magnetic/RestrictedRootedBlock.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Coordinate averaging for the actual rooted constrained block spin test.

  1. def OAI.InvariantIsing.cavityRootedBlockDepthTest line 14
  2. lemma OAI.InvariantIsing.cavityRootedBlockDepthTest_eq line 18
  3. lemma OAI.InvariantIsing.integral_cavityRootedBlockDepthTest line 26
  4. lemma OAI.InvariantIsing.restricted_rooted_block_evaluation line 37