OAI/Probability/InvariantIsing/Fields/FieldIncrementMgf.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exponential moment bounds for the actual scalar canonical transition kernels, including the unweighted root step.

  1. lemma OAI.InvariantIsing.fieldScalarLogCosh_dist_le line 16
  2. lemma OAI.InvariantIsing.fieldSpinTransition_exp_shift line 30
  3. theorem OAI.InvariantIsing.fieldTransitionKernel_mgf line 47
  4. theorem OAI.InvariantIsing.fieldScalarTransition_mgf line 58