OAI/Probability/InvariantIsing/Fields/FieldTailMgf.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Canonical endpoint exponential moments depend only on the sum of increment variances. Arbitrarily small positive exponents and arbitrarily many levels are allowed.

  1. def OAI.InvariantIsing.fieldTailVariance line 16
  2. lemma OAI.InvariantIsing.fieldTransitionKernel_integrable_exp line 19
  3. theorem OAI.InvariantIsing.fieldTailEndpointKernel_mgf line 30