OAI/Probability/InvariantIsing/Fields/FieldGaussianSemigroup.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Combining successive Gaussian increments with the same exponent. Both the log partition and the normalized transition retain their actual Gaussian laws, including zero variances and the ordinary exponent zero.

  1. lemma OAI.InvariantIsing.fieldGaussian_integral_comp line 17
  2. lemma OAI.InvariantIsing.exp_mul_gaussianOperator line 28
  3. theorem OAI.InvariantIsing.gaussianOperator_same_exponent line 42
  4. theorem OAI.InvariantIsing.fieldSpinTransition_same_exponent line 62