OAI/Probability/InvariantIsing/Cavity/RepeatedBlockSpinIdentity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Averaging the two-spin test over one constrained block equals its average over every site, and hence the total-overlap test.

  1. lemma OAI.InvariantIsing.restrictedCavityFullDisorderTest_const_mul line 16
  2. theorem OAI.InvariantIsing.repeated_block_spin_identity line 25