OAI/Probability/Ising/EdwardsSokal.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BufferedIsing.fkEdgeWeight line 12

   Source documentation

   Independent bond part of the comparison FK weight; the cluster factor is supplied by summing compatible fair cluster colors.

   noncomputable def fkEdgeWeight {n m : ℕ} (G : FiniteGraph n m)
       (F : Finset (Fin n)) (ω : Finset (Fin m)) : ℝ :=
   …

   Mentions: OAI.BufferedIsing.FiniteGraph

2. def OAI.BufferedIsing.jointColorWeight line 17
3. def OAI.BufferedIsing.comparisonSpinWeight line 21
4. lemma OAI.BufferedIsing.sum_jointColorWeight line 25
5. lemma OAI.BufferedIsing.sum_jointColorWeight_spin_product line 40
6. lemma OAI.BufferedIsing.sum_comparisonSpinWeight line 59
7. lemma OAI.BufferedIsing.sum_comparisonSpinWeight_spin_product line 67
8. lemma OAI.BufferedIsing.qZero_eq_color_correlation line 78

   Source documentation

   Finite Edwards–Sokal color averaging after vertex deletion and separate terminal contraction.

   lemma qZero_eq_color_correlation {n m : ℕ} (G : FiniteGraph n m)
       (I J F : Finset (Fin n)) (i j : KeptVertex F) :
       qZero G I J F i j =
         (∑ σ, comparisonSpinWeight G I J F σ * spin (σ i) * spin (σ j)) /
           ∑ σ, comparisonSpinWeight G I J F σ := by
   …

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

9. lemma OAI.BufferedIsing.sum_subsets_product line 86
10. def OAI.BufferedIsing.extendKept line 106

    Source documentation

    Extend a coloring from the vertex-DELETED graph. The values at deleted vertices are immaterial: every incident edge is absent from keptEdges.

    def extendKept {n : ℕ} (F : Finset (Fin n)) (σ : KeptVertex F → Bool) : Spins n :=
    …

    Mentions: OAI.BufferedIsing.KeptVertex, OAI.BufferedIsing.Spins

11. lemma OAI.BufferedIsing.extendKept_apply line 109
12. def OAI.BufferedIsing.BondCompatible line 114
13. lemma OAI.BufferedIsing.respects_comparison_iff line 118
14. lemma OAI.BufferedIsing.prod_conditioned_subset line 149
15. lemma OAI.BufferedIsing.jointColorWeight_expansion line 167
16. lemma OAI.BufferedIsing.comparisonSpinWeight_product line 193
17. lemma OAI.BufferedIsing.es_one_edge_identity line 222
18. def OAI.BufferedIsing.deletedEnergy line 228
19. def OAI.BufferedIsing.contractedZeroWeight line 235

    Source documentation

    Zero-field Ising weight on the vertex-deleted graph, with I,J separately contracted by restricting each to constant spin assignments.

    noncomputable def contractedZeroWeight {n m : ℕ} (G : FiniteGraph n m)
        (I J F : Finset (Fin n)) (σ : KeptVertex F → Bool) : ℝ :=
    …

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

20. lemma OAI.BufferedIsing.comparisonSpinWeight_eq_Ising line 239
21. lemma OAI.BufferedIsing.qZero_eq_zero_field_correlation line 252

    Source documentation

    The zero-field FK/Ising identity with vertex deletion, separate terminal contractions, and parallel edges.

    lemma qZero_eq_zero_field_correlation {n m : ℕ} (G : FiniteGraph n m)
        (I J F : Finset (Fin n)) (i j : KeptVertex F) :
        qZero G I J F i j =
          (∑ σ, contractedZeroWeight G I J F σ * spin (σ i) * spin (σ j)) /
            ∑ σ, contractedZeroWeight G I J F σ := by
    …

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