OAI/Probability/InvariantIsing/Cavity/CavityCutoffZero.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The cutoff/subtype identification also respects the zero convention when the original reference gives the cutoff no mass.

  1. lemma OAI.InvariantIsing.cavity_cutoff_replica_zero line 14
  2. theorem OAI.InvariantIsing.cavity_cutoff_replica_subtype_all line 28