OAI/Probability/InvariantIsing/Fields/FieldSquarePrefix.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Composition of an earlier conditional spin square with an unchanged later scalar recursion. This keeps the ordinary Gaussian root separate.

  1. def OAI.InvariantIsing.fieldPrefixIndex line 14
  2. lemma OAI.InvariantIsing.fieldScalarSquares_append_prefix line 18