OAI/Probability/InvariantIsing/Cavity/CavityLinearEnvelope.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform moments of the remaining linear cavity tilt. The estimate uses only the one-replica exponential radial moment after the quadratic tilt.

  1. def OAI.InvariantIsing.cavityLinearMomentEnvelope line 16
  2. lemma OAI.InvariantIsing.cavity_linear_logFactor_growth line 19
  3. lemma OAI.InvariantIsing.cavity_linear_envelope_bounds line 37
  4. theorem OAI.InvariantIsing.cavity_linear_tilt_radial_moment line 80
  5. theorem OAI.InvariantIsing.cavity_linear_tilt_mean_moment line 120