OAI/Probability/InvariantIsing/Fields/FieldScalarLogCoshSecond.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded first and second spatial derivatives for the scalar Ising backward recursion, including degenerate covariance increments.

  1. lemma OAI.InvariantIsing.field_hasDerivAt_tanh line 14
  2. lemma OAI.InvariantIsing.field_tanh_second_bound line 23
  3. theorem OAI.InvariantIsing.fieldScalarLogCoshSecond_regular line 28
  4. theorem OAI.InvariantIsing.hasDerivAt_fieldScalarLogCoshMean line 42