OAI/Probability/InvariantIsing/Magnetic/RestrictedEndpointTest.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Coordinate spin tests of the constrained endpoint law. These are consequences of the published marking input and the actual spin kernels.

  1. def OAI.InvariantIsing.restrictedTerminalPairMean line 16
  2. lemma OAI.InvariantIsing.measurable_restrictedTerminalPairMean line 21
  3. lemma OAI.InvariantIsing.restrictedTerminalPairMean_bound line 30
  4. lemma OAI.InvariantIsing.restrictedPairCoordinateMean_endpoint line 41
  5. def OAI.InvariantIsing.restrictedEndpointCoordinateTest line 51
  6. lemma OAI.InvariantIsing.measurable_restrictedEndpointCoordinateTest line 56
  7. lemma OAI.InvariantIsing.restrictedEndpointCoordinateTest_bound line 63
  8. theorem OAI.InvariantIsing.restricted_field_published_coordinate_test line 73