OAI/Probability/InvariantIsing/Fields/FieldFiniteMoments.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Uniform Gaussian tilted moments for the finite height family.

  1. lemma OAI.InvariantIsing.FieldFiniteFamily.spatial_abs_sub_le line 13
  2. lemma OAI.InvariantIsing.FieldFiniteFamily.shifted_second_moment line 21
  3. def OAI.InvariantIsing.FieldFiniteFamily.affineShift line 63
  4. def OAI.InvariantIsing.FieldFiniteFamily.affineDifferential line 66
  5. def OAI.InvariantIsing.FieldFiniteFamily.affineLaw line 70
  6. lemma OAI.InvariantIsing.FieldFiniteFamily.affineLaw_probability line 73
  7. lemma OAI.InvariantIsing.FieldFiniteFamily.affineLaw_quadratic_moment line 81
  8. def OAI.InvariantIsing.FieldFiniteFamily.affineMomentCap line 90
  9. lemma OAI.InvariantIsing.FieldFiniteFamily.affineMomentCap_pos line 93
  10. lemma OAI.InvariantIsing.FieldFiniteFamily.affineLaw_moment_le line 97
  11. lemma OAI.InvariantIsing.FieldFiniteFamily.affineLaw_integral_bound line 105
  12. lemma OAI.InvariantIsing.FieldFiniteFamily.affineLaw_linear_integrable line 113
  13. lemma OAI.InvariantIsing.FieldFiniteFamily.affineLaw_bounded_integrable line 121