OAI/Probability/InvariantIsing/Magnetic/RestrictedPairMoments.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Conditional coordinate means in the constrained block and their actual two-spin interpretation.

  1. def OAI.InvariantIsing.restrictedCoordinateMean line 14
  2. def OAI.InvariantIsing.restrictedPairCoordinateMean line 19
  3. lemma OAI.InvariantIsing.measurable_restrictedCoordinateMean line 24
  4. lemma OAI.InvariantIsing.measurable_restrictedPairCoordinateMean line 33
  5. lemma OAI.InvariantIsing.restrictedCoordinateMean_bound line 43
  6. lemma OAI.InvariantIsing.restrictedPairCoordinateMean_bound line 54
  7. lemma OAI.InvariantIsing.restrictedPairSpinKernel_zero line 65
  8. lemma OAI.InvariantIsing.restrictedPairCoordinateMean_zero line 72