OAI/Probability/InvariantIsing/Arrays/CoordinatePairData.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The measurable labeled two-path observable in the original forest coordinates.

  1. def OAI.InvariantIsing.coordinatePairData line 11
  2. lemma OAI.InvariantIsing.measurable_coordinatePairData line 16