OAI/Probability/InvariantIsing/Fields/FieldSpinDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Spatial differentiation of the scalar Gaussian operator. The payoff may grow linearly; only its derivative is bounded.

  1. lemma OAI.InvariantIsing.fieldSpinTransition_eq_shifted line 15
  2. lemma OAI.InvariantIsing.gaussianOperator_eq_logMean_shift line 25
  3. lemma OAI.InvariantIsing.hasDerivAt_gaussianOperator line 33