OAI/Probability/InvariantIsing/Cavity/CavityOrderedGroups.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Canonical ordered finite spectral groups are literal contiguous windows. This fixes the full/base spectral ordering in the rational cavity sequence.

  1. def OAI.InvariantIsing.cavityOrderedStart line 13
  2. def OAI.InvariantIsing.cavityOrderedEquiv line 16
  3. def OAI.InvariantIsing.cavityOrderedGroup line 20
  4. lemma OAI.InvariantIsing.cavityOrderedGroup_congr line 23
  5. lemma OAI.InvariantIsing.cavityOrderedEquiv_val line 29
  6. lemma OAI.InvariantIsing.cavityOrderedGroup_window line 35
  7. lemma OAI.InvariantIsing.cavityOrderedGroup_card line 59
  8. lemma OAI.InvariantIsing.cavityOrderedStart_add_le line 64