OAI/Probability/InvariantIsing/Cavity/CavityOriginalFactor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact cavity reweighting of the original perturbed spin model. Both Hamiltonians contain the same Gaussian disorder coordinate.

  1. def OAI.InvariantIsing.cavityRotationHamiltonian line 14
  2. lemma OAI.InvariantIsing.cavity_rotation_exp_integrable_ae line 19
  3. def OAI.InvariantIsing.cavityOriginalFactor line 34
  4. theorem OAI.InvariantIsing.cavity_original_replica_factorization line 43
  5. lemma OAI.InvariantIsing.cavityOriginalFactor_decomposition line 65