OAI/Probability/InvariantIsing/Cavity/CavityNormalizerProbability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Convergence in probability of a quadratic coefficient error controls capped normalizers in mean, using the actual prior fourth moment.

  1. theorem OAI.InvariantIsing.cavity_capped_normalizer_probability_limit line 15