OAI/Probability/InvariantIsing/Magnetic/MagneticScalarContinuation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The literal conditional squared means of the finite Ising recursion have bounded spatial derivatives through order three. The ordinary root Gaussian is retained in the statement.

  1. def OAI.InvariantIsing.magneticLogCoshMeanJet line 16
  2. theorem OAI.InvariantIsing.fieldScalarSquares_has_bounded_jet line 53
  3. theorem OAI.InvariantIsing.magneticLevelAtBias_has_bounded_jet line 74