OAI/Probability/InvariantIsing/Cavity/CavityCoefficientProbability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A bounded continuous test detects deviations of the three cavity coefficients. Weak convergence to deterministic coefficients therefore gives the probability estimate required by the replica comparison.

  1. def OAI.InvariantIsing.cavityFactorDeviation line 15
  2. lemma OAI.InvariantIsing.continuous_cavityFactorDeviation line 18
  3. lemma OAI.InvariantIsing.cavityFactorDeviation_nonneg line 31
  4. lemma OAI.InvariantIsing.cavityFactorDeviation_self line 34
  5. def OAI.InvariantIsing.cavityFactorDeviationTest line 38
  6. theorem OAI.InvariantIsing.cavity_factor_coefficients_probability line 48