OAI/Probability/InvariantIsing/Cavity/CavityHaarRestrictedNumerator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The physical hard-restricted numerator is the fresh-Haar test under the infinite replica law, retaining the common original disorder.

  1. lemma OAI.InvariantIsing.measurable_cavityRestrictedHaarReplicaValue line 16
  2. theorem OAI.InvariantIsing.cavity_haar_restricted_spin_numerator_average line 45