OAI/Probability/InvariantIsing/Cavity/CavityHaarSpinModel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The measurable physical cavity model, with original disorder and fresh Haar frames outside the replica prior.

  1. def OAI.InvariantIsing.cavityHaarSpinPriorKernel line 15
  2. lemma OAI.InvariantIsing.cavityHaarSpinPriorKernel_apply line 23
  3. instance OAI.InvariantIsing.cavityHaarSpinPriorKernel_isMarkov line 34
  4. def OAI.InvariantIsing.cavityHaarSpinPotential line 44
  5. lemma OAI.InvariantIsing.measurable_cavityHaarSpinPotential line 53
  6. def OAI.InvariantIsing.cavityHaarSpinReplicaTest line 70
  7. lemma OAI.InvariantIsing.measurable_cavityHaarSpinReplicaTest line 76
  8. lemma OAI.InvariantIsing.cavityHaarSpinReplicaTest_bound line 90