OAI/Probability/InvariantIsing/Fields/FieldTiltAverageDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Differentiation of the scalar tilted spin average. The potential needs an exponential moment at the base point, rather than a global bound.

  1. lemma OAI.InvariantIsing.parameter_exp_bound line 14
  2. theorem OAI.InvariantIsing.hasDerivAt_tiltAverage_of_bounded_derivatives line 34