OAI/Probability/InvariantIsing/Magnetic/MagneticScalarThird.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The third spatial derivative propagated through the finite scalar recursion, with an explicit finite bound at every level.

  1. def OAI.InvariantIsing.fieldScalarThird line 14
  2. def OAI.InvariantIsing.fieldScalarThirdCap line 21
  3. lemma OAI.InvariantIsing.fieldScalarThird_regular line 26
  4. lemma OAI.InvariantIsing.hasDerivAt_fieldScalarSecond line 46
  5. lemma OAI.InvariantIsing.field_logCosh_third_derivative line 71
  6. lemma OAI.InvariantIsing.field_logCosh_third_bound line 82
  7. lemma OAI.InvariantIsing.hasDerivAt_fieldScalarLogCoshSecond line 97