OAI/Probability/Ising/RandomCluster.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BufferedIsing.fkWeight_nonneg line 9
2. lemma OAI.BufferedIsing.fkWeight_empty_pos line 23
3. lemma OAI.BufferedIsing.comparison_empty_preserves_I line 30
4. lemma OAI.BufferedIsing.qZero_nonneg_lt_one line 46
5. lemma OAI.BufferedIsing.comparisonRel_terminal_swap line 76
6. lemma OAI.BufferedIsing.qZero_terminal_swap line 85

   Source documentation

   The zero-field terminal connection probability is symmetric under exchange of the terminal sets.

   lemma qZero_terminal_swap {n m : ℕ} (G : FiniteGraph n m)
       (I J F : Finset (Fin n)) (i j : KeptVertex F) :
       qZero G I J F i j = qZero G J I F j i := by
   …

   Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.KeptVertex, OAI.BufferedIsing.qZero

7. lemma OAI.BufferedIsing.qZero_independent_representatives line 107