OAI/Probability/InvariantIsing/Fields/FieldGaussianTerminal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

At exponent one the Gaussian log-cosh operator adds only a constant. This is the terminal endpoint of the adjacent-variance comparison.

  1. lemma OAI.InvariantIsing.fieldGaussian_integral_cosh line 15
  2. lemma OAI.InvariantIsing.gaussianOperator_one_logCosh line 30
  3. lemma OAI.InvariantIsing.fieldSpinTransition_one_tanh line 41
  4. lemma OAI.InvariantIsing.fieldSpinTransition_const_add line 59