OAI/Probability/InvariantIsing/Cavity/CavityCoefficientError.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Quantitative replacement of the finite cavity blocks by their limits. The energy cap keeps the exponential Lipschitz constant independent of the Gaussian marks; only their second moments enter the remaining error.

  1. lemma OAI.InvariantIsing.cavity_exp_sub_le line 15
  2. lemma OAI.InvariantIsing.cavity_capped_exp_sub_le line 37
  3. lemma OAI.InvariantIsing.cavityLogFactor_sub line 44
  4. theorem OAI.InvariantIsing.cavity_capped_replica_coefficient_error line 53