OAI/Probability/InvariantIsing/Cavity/CavityPhysicalFactor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The cavity exponent difference in the original coordinates. The retained interaction cancels; only the special and cavity projections enter the factor.

  1. lemma OAI.InvariantIsing.cavityQuadratic_dotProduct line 14
  2. lemma OAI.InvariantIsing.cavityQuadratic_add line 19
  3. lemma OAI.InvariantIsing.cavityQuadratic_transpose line 24
  4. lemma OAI.InvariantIsing.cavityQuadratic_rectangular line 30
  5. def OAI.InvariantIsing.cavityPhysicalChange line 38
  6. theorem OAI.InvariantIsing.cavityPhysicalChange_factor line 45
  7. theorem OAI.InvariantIsing.cavityPhysicalChange_energy_difference line 61