OAI/Probability/InvariantIsing/Arrays/PathSymbolAEUniqueness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Almost-everywhere symbols determine the almost-everywhere path up to one constant. This is the form needed after weak limiting Ward equations.

  1. theorem OAI.InvariantIsing.ae_equal_pathSymbols_constant_difference line 15
  2. lemma OAI.InvariantIsing.ae_constant_right_root line 72
  3. theorem OAI.InvariantIsing.ae_equal_pathSymbols_equal_roots line 94