OAI/Probability/InvariantIsing/Cavity/CavityReplicaCutoff.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Explicit normalization of a cutoff in a bounded two-replica test. The ratio convention also covers an empty cutoff.

  1. def OAI.InvariantIsing.cavityCutoffReplicaMean line 15
  2. lemma OAI.InvariantIsing.measurable_cavityCutoffReplicaMean line 20
  3. lemma OAI.InvariantIsing.cavity_cutoff_replica_eq_cond line 39
  4. theorem OAI.InvariantIsing.cavity_cutoff_replica_error line 65
  5. lemma OAI.InvariantIsing.cavity_reference_tail_eq line 79