OAI/Probability/InvariantIsing/Magnetic/RestrictedCoordinateOverlap.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Coordinate overlap paths for the actual constrained scalar-field law.

  1. def OAI.InvariantIsing.restrictedCoordinatePairMean line 13
  2. lemma OAI.InvariantIsing.restrictedCoordinatePairMean_mem_unit line 20
  3. lemma OAI.InvariantIsing.restrictedCoordinatePairMean_monotone line 33
  4. def OAI.InvariantIsing.restrictedCoordinateOverlapPath line 41
  5. lemma OAI.InvariantIsing.restrictedBlockOverlapPath_eq_average line 47