OAI/Probability/InvariantIsing/Cavity/CavityUniformComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform covariance comparison on a fixed cavity cutoff. The bound also holds after adding any common bounded replica-test energy.

  1. lemma OAI.InvariantIsing.cylinder_log_mean_const_add line 13
  2. lemma OAI.InvariantIsing.countable_cylinder_covariance_mean_le line 34
  3. theorem OAI.InvariantIsing.countable_cylinder_uniform_comparison line 55