OAI/Probability/InvariantIsing/Magnetic/MagneticSquareInitial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact initial square data for the induction over Gaussian levels.

  1. lemma OAI.InvariantIsing.closedMagneticSquareContinuation_zero_initial line 13
  2. lemma OAI.InvariantIsing.closedMagneticSquareContinuation_cons_initial line 30
  3. lemma OAI.InvariantIsing.magneticScaledSquareContinuation_zero_initial line 50
  4. lemma OAI.InvariantIsing.magneticScaledSquareContinuation_cons_initial line 59