OAI/Probability/InvariantIsing/Fields/PhysicalFieldPermutation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A deterministic permutation of field sites preserves the physical Haar mean.

  1. def OAI.InvariantIsing.fieldSitePermutation line 13
  2. lemma OAI.InvariantIsing.spinVector_fieldSitePermutation line 16
  3. lemma OAI.InvariantIsing.rotatedPressure_fieldSitePermutation line 24
  4. lemma OAI.InvariantIsing.physical_meanPressure_field_permutation line 50