OAI/Probability/InvariantIsing/Magnetic/MagneticScalarFourJet.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Every actual finite scalar Ising mean, and every continued square observable, has the fourth spatial derivative required in the parabolic comparison. No additional smoothness hypothesis is imposed on the model.

  1. def OAI.InvariantIsing.logCoshMeanFourJet line 16
  2. lemma OAI.InvariantIsing.fieldScalarMean_has_bounded_fourJet line 45
  3. def OAI.InvariantIsing.magneticLogCoshMeanFourJet line 64
  4. lemma OAI.InvariantIsing.magneticLogCoshMeanFourJet_eq line 68
  5. lemma OAI.InvariantIsing.fieldScalarSquares_has_bounded_fourJet line 74