OAI/Probability/InvariantIsing/Fields/FieldTerminalGenerator.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The terminal Ising identity gives the constant term at the last covariance level of the backward derivative.

  1. lemma OAI.InvariantIsing.field_tanh_generator_one line 15
  2. lemma OAI.InvariantIsing.field_tanh_generator line 22
  3. lemma OAI.InvariantIsing.fieldSpinTransition_terminal_generator line 28