OAI/Probability/Ising/Basic.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BufferedIsing.FiniteGraph line 11

   Source documentation

   A finite graph given by its edge list. Zero couplings can encode missing edges. Edges are indexed separately so parallel edges are counted separately.

   Also declared: ComparatorChallenges/BufferedIsing.lean:11 (same declaration text).

   structure FiniteGraph (n m : ℕ) where
   …

2. abbrev OAI.BufferedIsing.Spins line 18

   Also declared: ComparatorChallenges/BufferedIsing.lean:18 (same declaration text).

3. def OAI.BufferedIsing.spin line 20

   Also declared: ComparatorChallenges/BufferedIsing.lean:20 (same declaration text).

4. def OAI.BufferedIsing.energy line 22

   Also declared: ComparatorChallenges/BufferedIsing.lean:22 (same declaration text).

5. def OAI.BufferedIsing.weight line 27

   Also declared: ComparatorChallenges/BufferedIsing.lean:27 (same declaration text).

6. def OAI.BufferedIsing.AgreesOn line 30

   Also declared: ComparatorChallenges/BufferedIsing.lean:30 (same declaration text).

7. def OAI.BufferedIsing.constrainedSum line 33

   Also declared: ComparatorChallenges/BufferedIsing.lean:33 (same declaration text).

8. def OAI.BufferedIsing.conditionalProb line 40

   Source documentation

   Conditional probability of σ_I=a, with σ_J=b and σ_F=τ prescribed. All sums are finite and all fields are finite real numbers.

   Also declared: ComparatorChallenges/BufferedIsing.lean:40 (same declaration text).

   noncomputable def conditionalProb {n m : ℕ} (G : FiniteGraph n m)
       (h : Fin n → ℝ) (I J F : Finset (Fin n)) (a b τ : Spins n) : ℝ :=
   …

   Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.Spins

9. def OAI.BufferedIsing.keptEdges line 46

   Source documentation

   Edges remaining after DELETION, not pinning, of F.

   Also declared: ComparatorChallenges/BufferedIsing.lean:46 (same declaration text).

   def keptEdges {n m : ℕ} (G : FiniteGraph n m) (F : Finset (Fin n)) : Finset (Fin m) :=
   …

   Mentions: OAI.BufferedIsing.FiniteGraph

10. abbrev OAI.BufferedIsing.KeptVertex line 49

    Also declared: ComparatorChallenges/BufferedIsing.lean:49 (same declaration text).

11. def OAI.BufferedIsing.comparisonRel line 53

    Source documentation

    Open-edge adjacency together with the two separate terminal identifications. No virtual identification of common pins is present: those vertices are absent.

    Also declared: ComparatorChallenges/BufferedIsing.lean:53 (same declaration text).

    def comparisonRel {n m : ℕ} (G : FiniteGraph n m)
        (I J F : Finset (Fin n)) (ω : Finset (Fin m)) (u v : KeptVertex F) : Prop :=
    …

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

12. def OAI.BufferedIsing.comparisonSetoid line 60

    Source documentation

    The equivalence closure implements components of the contracted open graph.

    Also declared: ComparatorChallenges/BufferedIsing.lean:60 (same declaration text).

    def comparisonSetoid {n m : ℕ} (G : FiniteGraph n m)
        (I J F : Finset (Fin n)) (ω : Finset (Fin m)) : Setoid (KeptVertex F) :=
    …

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

13. def OAI.BufferedIsing.clusterCount line 64

    Also declared: ComparatorChallenges/BufferedIsing.lean:64 (same declaration text).

14. def OAI.BufferedIsing.fkWeight line 72

    Source documentation

    Zero-field FK weight with q=2 and p_e=1-exp(-2 K_e). Parallel edges may be retained: the measure after summing them is the measure for the summed parallel coupling. Loops created by contraction do not change components and cancel from connection probabilities.

    Also declared: ComparatorChallenges/BufferedIsing.lean:72 (same declaration text).

    noncomputable def fkWeight {n m : ℕ} (G : FiniteGraph n m)
        (I J F : Finset (Fin n)) (ω : Finset (Fin m)) : ℝ := by
    …

    Mentions: OAI.BufferedIsing.FiniteGraph

15. def OAI.BufferedIsing.qZero line 81

    Source documentation

    Choose any i in I and j in J. The terminal connection is independent of these choices because I and J are each identified.

    Also declared: ComparatorChallenges/BufferedIsing.lean:81 (same declaration text).

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

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

16. def OAI.BufferedIsing.mixtureProb line 91

    Source documentation

    Any probability mixture of source prescriptions. Full configurations index the mixture, but only their restrictions to J are used. Thus this is exactly the class of all mixtures on {-1,+1}^J.

    Also declared: ComparatorChallenges/BufferedIsing.lean:91 (same declaration text).

    noncomputable def mixtureProb {n m : ℕ} (G : FiniteGraph n m)
        (h : Fin n → ℝ) (I J F : Finset (Fin n)) (a τ : Spins n)
        (mix : Spins n → ℝ) : ℝ :=
    …

    Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.Spins

17. lemma OAI.BufferedIsing.spin_true line 96
18. lemma OAI.BufferedIsing.spin_false line 97
19. def OAI.BufferedIsing.jointWeight line 100

    Source documentation

    The unnormalized I,J marginal with the common pins F fixed.

    noncomputable def jointWeight {n m : ℕ} (G : FiniteGraph n m)
        (h : Fin n → ℝ) (I J F : Finset (Fin n)) (τ a b : Spins n) : ℝ :=
    …

    Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.Spins

20. def OAI.BufferedIsing.expectation line 105

    Source documentation

    Expectation in the unpinned finite Ising law.

    noncomputable def expectation {n m : ℕ} (G : FiniteGraph n m)
        (h : Fin n → ℝ) (f : Spins n → ℝ) : ℝ :=
    …

    Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.Spins

21. def OAI.BufferedIsing.ArbitraryFieldCovarianceBound line 110

    Source documentation

    Arbitrary real background fields do not increase the spin covariance above the zero-field correlation.

    def ArbitraryFieldCovarianceBound : Prop :=
    …

22. lemma OAI.BufferedIsing.weight_pos line 116
23. lemma OAI.BufferedIsing.constrainedSum_nonneg line 119
24. lemma OAI.BufferedIsing.constrainedSum_pos line 128
25. lemma OAI.BufferedIsing.jointWeight_pos line 139
26. lemma OAI.BufferedIsing.spin_modular line 156
27. lemma OAI.BufferedIsing.spin_product_supermodular line 160
28. lemma OAI.BufferedIsing.energy_supermodular line 165
29. lemma OAI.BufferedIsing.weight_logSupermodular line 189
30. lemma OAI.BufferedIsing.agreesOn_inf line 196
31. lemma OAI.BufferedIsing.agreesOn_sup line 201