OAI/Probability/InvariantIsing/Cavity/CavityCutoffNormalizer.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A cutoff weight is bounded below whenever the discarded prior mass is at most one half. The exceptional event is controlled by its mean.

  1. lemma OAI.InvariantIsing.cavity_cutoff_normalizer_lower line 14
  2. lemma OAI.InvariantIsing.cavity_cutoff_normalizer_half line 38
  3. lemma OAI.InvariantIsing.cavity_small_normalizer_probability line 46