OAI/Probability/InvariantIsing/Fields/FieldSpinLinear.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Linear identities for the actual tilted scalar transition.

  1. lemma OAI.InvariantIsing.fieldSpinTransition_const_mul line 13
  2. lemma OAI.InvariantIsing.fieldSpinTransition_add line 18
  3. lemma OAI.InvariantIsing.fieldSpinTransition_const line 32
  4. lemma OAI.InvariantIsing.fieldSpinTransition_generator_difference line 41