OAI/Probability/InvariantIsing/Magnetic/MagneticScalarFourth.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual fourth spatial derivative through every finite backward level. Its global bound is finite for each fixed finite field.

  1. def OAI.InvariantIsing.fieldScalarFourth line 14
  2. lemma OAI.InvariantIsing.fieldScalarFourth_regular line 22
  3. lemma OAI.InvariantIsing.hasDerivAt_fieldScalarThird line 44
  4. def OAI.InvariantIsing.fieldLogCoshFourth line 75
  5. lemma OAI.InvariantIsing.field_logCosh_fourth_derivative line 79
  6. lemma OAI.InvariantIsing.field_logCosh_fourth_bound line 91
  7. lemma OAI.InvariantIsing.hasDerivAt_fieldScalarLogCoshThird line 113