OAI/Probability/InvariantIsing/Arrays/TripleContractions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Replica contractions for the off-diagonal spectral Ward equation.

  1. def OAI.InvariantIsing.gibbsTripleAverage line 16
  2. lemma OAI.InvariantIsing.gibbsPairAverage_mul_gibbsAverage line 19
  3. lemma OAI.InvariantIsing.gibbsPairAverage_sub line 34
  4. lemma OAI.InvariantIsing.gibbsTripleAverage_finset_sum line 39
  5. lemma OAI.InvariantIsing.off_direct_contraction line 57
  6. lemma OAI.InvariantIsing.off_subtraction_contraction line 75
  7. lemma OAI.InvariantIsing.off_difference_contraction line 93