OAI/Probability/InvariantIsing/Cavity/CavityTruncation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform covariance bounds for the monomials omitted when the perturbation cutoff changes by a fixed cavity size.

  1. lemma OAI.InvariantIsing.cavity_weighted_kernel_abs_le line 15
  2. lemma OAI.InvariantIsing.cavity_weighted_kernel_tail_le line 38
  3. lemma OAI.InvariantIsing.cavity_covariance_mass_difference line 60
  4. theorem OAI.InvariantIsing.cavity_covariance_cutoff_error_tendsto line 72