OAI/Probability/Ising/Colorings.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BufferedIsing.spin_not line 9
2. lemma OAI.BufferedIsing.spin_sq line 12
3. def OAI.BufferedIsing.Respects line 16

   Source documentation

   A coloring is constant on precisely the components specified by a setoid.

   def Respects {V : Type*} (S : Setoid V) (σ : V → Bool) : Prop :=
   …

4. abbrev OAI.BufferedIsing.Colorings line 19
5. instance OAI.BufferedIsing.coloringsFintype line 21
6. def OAI.BufferedIsing.componentColoringEquiv line 25

   Source documentation

   The exact bijection underlying the factor 2^(number of FK clusters).

   def componentColoringEquiv {V : Type*} (S : Setoid V) :
       Colorings S ≃ (Quotient S → Bool) where
   …

   Mentions: OAI.BufferedIsing.Colorings

7. lemma OAI.BufferedIsing.card_colorings line 34
8. def OAI.BufferedIsing.flipAt line 40
9. lemma OAI.BufferedIsing.flipAt_apply line 50
10. lemma OAI.BufferedIsing.sum_spin_product line 55
11. lemma OAI.BufferedIsing.sum_if_respects line 71
12. lemma OAI.BufferedIsing.sum_respects_one line 77
13. lemma OAI.BufferedIsing.sum_respects_spin_product line 84
14. lemma OAI.BufferedIsing.respects_eqvGen line 96