OAI/Probability/InvariantIsing/Cavity/CavityQuadraticCompression.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Quadratic energies in physical coordinates and after deleting the annihilated cavity rows and columns.

  1. lemma OAI.InvariantIsing.cavityQuadratic_conjugate line 14
  2. lemma OAI.InvariantIsing.cavityQuadratic_first_block line 22
  3. lemma OAI.InvariantIsing.cavityQuadratic_first_block_of_symmetric line 33
  4. lemma OAI.InvariantIsing.cavityQuadratic_diagonal line 44
  5. lemma OAI.InvariantIsing.cavity_rotatedEnergy_matrix line 53
  6. lemma OAI.InvariantIsing.cavityQuadratic_inverse_rotation line 62
  7. lemma OAI.InvariantIsing.cavityBaseReplacement_transpose line 70