OAI/Probability/Ising/Contraction.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BufferedIsing.PairInteraction line 10

   Source documentation

   A finite pair interaction allowing self-loops and arbitrary vertex and edge labels.

   structure PairInteraction (V E : Type*) where
   …

2. def OAI.BufferedIsing.interactionEnergy line 16
3. def OAI.BufferedIsing.interactionWeight line 21
4. abbrev OAI.BufferedIsing.NonloopEdge line 25
5. def OAI.BufferedIsing.interactionLoopConstant line 28
6. def OAI.BufferedIsing.interactionGraph line 33

   Source documentation

   Relabeling a finite loop-deleted interaction by Fin does not introduce any assumption on the fields or on connectivity. Parallel edges are kept.

   noncomputable def interactionGraph {V E : Type*} [Fintype V] [Fintype E]
       (P : PairInteraction V E) :
       FiniteGraph (Fintype.card V) (Fintype.card (NonloopEdge P)) where
   …

   Mentions: OAI.BufferedIsing.PairInteraction, OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.NonloopEdge

7. lemma OAI.BufferedIsing.sum_nonloop line 45
8. lemma OAI.BufferedIsing.interactionEnergy_relabel line 52
9. lemma OAI.BufferedIsing.interactionWeight_relabel line 78
10. lemma OAI.BufferedIsing.pairTable_relabel line 89

    Source documentation

    Marginal tables commute with a bijective change of vertex labels.

    lemma pairTable_relabel {V W : Type*} [Fintype V] [Fintype W]
        [DecidableEq V] [DecidableEq W] (e : V ≃ W) (f : (V → Bool) → ℝ)
        (u v : V) (s t : Bool) :
        pairTable (fun σ : W → Bool => f (fun x => σ (e x))) (e u) (e v) s t =
          pairTable f u v s t := by
    …

    Mentions: OAI.BufferedIsing.pairTable

11. lemma OAI.BufferedIsing.pairTable_scale line 101
12. lemma OAI.BufferedIsing.tableCoupling_scale line 111
13. lemma OAI.BufferedIsing.pairTable_pos_of_weight_pos line 116
14. lemma OAI.BufferedIsing.pairTable_quotient line 130
15. abbrev OAI.BufferedIsing.ContractedVertex line 150
16. abbrev OAI.BufferedIsing.KeptEdge line 153
17. def OAI.BufferedIsing.edgeLeftKept line 156
18. def OAI.BufferedIsing.edgeRightKept line 160
19. def OAI.BufferedIsing.contractedInteraction line 164
20. def OAI.BufferedIsing.quotientField line 174

    Source documentation

    The contracted finite field is the SUM of the fields in the identified class. Common fixed spins have already been removed and contribute through pinField; opposite common signs are never wired together.

    noncomputable def quotientField {V : Type*} [Fintype V] (S : Setoid V)
        (h : V → ℝ) (q : Quotient S) : ℝ := ∑ v, if Quotient.mk S v = q then h v else 0

21. lemma OAI.BufferedIsing.quotientField_sum line 177
22. lemma OAI.BufferedIsing.quotientField_zero line 188
23. lemma OAI.BufferedIsing.contractedInteraction_energy line 193
24. lemma OAI.BufferedIsing.contractedPinned_quotient_weight line 212
25. lemma OAI.BufferedIsing.contractedPinned_pairTable_quotient line 223
26. lemma OAI.BufferedIsing.contractedZero_pairTable_quotient line 236
27. lemma OAI.BufferedIsing.interactionGraph_pairTable line 256
28. lemma OAI.BufferedIsing.interactionGraph_coupling line 270
29. lemma OAI.BufferedIsing.contractedTerminal_ne line 288
30. def OAI.BufferedIsing.actualComparisonGraph line 296
31. def OAI.BufferedIsing.actualComparisonField line 299
32. def OAI.BufferedIsing.actualTerminal line 304
33. lemma OAI.BufferedIsing.actualTerminal_ne line 308
34. lemma OAI.BufferedIsing.extremeLogOdds_eq_actualCoupling line 316

    Source documentation

    The extreme log odds equals four times the effective coupling after deletion and separate terminal contraction, with fields induced by the common pins.

    lemma extremeLogOdds_eq_actualCoupling {n m : ℕ} (G : FiniteGraph n m)
        (h : Fin n → ℝ) (I J F : Finset (Fin n))
        (hIJ : Disjoint I J) (hIF : Disjoint I F) (hJF : Disjoint J F)
        (i j : KeptVertex F) (hi : i.val ∈ I) (hj : j.val ∈ J) (τ : Spins n) :
        extremeLogOdds G h I J F τ = 4 * tableCoupling (pairTable
          (weight (actualComparisonGraph G I J F) (actualComparisonField G h I J F τ))
          (actualTerminal G I J F i) (actualTerminal G I J F j)) := by
    …

    Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.KeptVertex, OAI.BufferedIsing.Spins, OAI.BufferedIsing.extremeLogOdds, OAI.BufferedIsing.tableCoupling, OAI.BufferedIsing.pairTable, OAI.BufferedIsing.weight, OAI.BufferedIsing.actualComparisonGraph, OAI.BufferedIsing.actualComparisonField, OAI.BufferedIsing.actualTerminal

35. lemma OAI.BufferedIsing.artanh_qZero_eq_actualCoupling line 343

    Source documentation

    The inverse hyperbolic tangent of the FK connection probability equals the zero-field coupling on the deleted, separately contracted graph.

    lemma artanh_qZero_eq_actualCoupling {n m : ℕ} (G : FiniteGraph n m)
        (I J F : Finset (Fin n)) (hIJ : Disjoint I J)
        (i j : KeptVertex F) (hi : i.val ∈ I) (hj : j.val ∈ J) :
        Real.artanh (qZero G I J F i j) = tableCoupling (pairTable
          (weight (actualComparisonGraph G I J F) (fun _ => 0))
          (actualTerminal G I J F i) (actualTerminal G I J F j)) := by
    …

    Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.KeptVertex, OAI.BufferedIsing.qZero, OAI.BufferedIsing.tableCoupling, OAI.BufferedIsing.pairTable, OAI.BufferedIsing.weight, OAI.BufferedIsing.actualComparisonGraph, OAI.BufferedIsing.actualTerminal