OAI/Probability/InvariantIsing/Magnetic/MagneticContinuationJet.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A bounded third-order spatial jet for the finite Ising continuation. Only the square and actual Gaussian transition operations are required.

  1. structure OAI.InvariantIsing.MagneticContinuationJet line 14
  2. def OAI.InvariantIsing.MagneticContinuationJet.square line 33
  3. def OAI.InvariantIsing.MagneticContinuationJet.transition line 64