OAI/Probability/InvariantIsing/Core/FiniteFieldMatchingBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The unmatched field sites are controlled by differences of label counts.

  1. lemma OAI.InvariantIsing.fieldLabelCount_sum line 10
  2. theorem OAI.InvariantIsing.exists_field_permutation_l1_bound line 15