OAI/Probability/SKGap/Model.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SKGap.Spin line 11

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

2. abbrev OAI.SKGap.Edge line 12

   Also declared: ComparatorChallenges/SKHighTemperature.lean:12 (same declaration text).

3. abbrev OAI.SKGap.Disorder line 13

   Also declared: ComparatorChallenges/SKHighTemperature.lean:13 (same declaration text).

4. def OAI.SKGap.spinValue line 15

   Also declared: ComparatorChallenges/SKHighTemperature.lean:15 (same declaration text).

5. def OAI.SKGap.coupling line 17

   Also declared: ComparatorChallenges/SKHighTemperature.lean:17 (same declaration text).

6. def OAI.SKGap.hamiltonian line 21

   Also declared: ComparatorChallenges/SKHighTemperature.lean:21 (same declaration text).

7. def OAI.SKGap.weight line 25

   Also declared: ComparatorChallenges/SKHighTemperature.lean:25 (same declaration text).

8. def OAI.SKGap.partition line 28

   Also declared: ComparatorChallenges/SKHighTemperature.lean:28 (same declaration text).

9. def OAI.SKGap.mass line 31

   Also declared: ComparatorChallenges/SKHighTemperature.lean:31 (same declaration text).

10. def OAI.SKGap.expectation line 34

    Also declared: ComparatorChallenges/SKHighTemperature.lean:34 (same declaration text).

11. def OAI.SKGap.variance line 37

    Also declared: ComparatorChallenges/SKHighTemperature.lean:37 (same declaration text).

12. def OAI.SKGap.flip line 40

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

13. def OAI.SKGap.conditionalExpectation line 44

    Source documentation

    Conditional expectation under the actual Gibbs law given all other spins.

    Also declared: ComparatorChallenges/SKHighTemperature.lean:44 (same declaration text).

    def conditionalExpectation {n : ℕ} (g : Disorder n) (h : Fin n → ℝ)
        (i : Fin n) (f : Spin n → ℝ) (x : Spin n) : ℝ :=
    …

    Mentions: OAI.SKGap.Disorder, OAI.SKGap.Spin

14. def OAI.SKGap.dirichlet line 50

    Source documentation

    Unscaled form: each site has a rate-one clock.

    Also declared: ComparatorChallenges/SKHighTemperature.lean:50 (same declaration text).

    def dirichlet {n : ℕ} (g : Disorder n) (h : Fin n → ℝ) (f : Spin n → ℝ) : ℝ :=
    …

    Mentions: OAI.SKGap.Disorder, OAI.SKGap.Spin

15. def OAI.SKGap.disorderLaw line 53

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

16. def OAI.SKGap.poincareEvent line 56

    Also declared: ComparatorChallenges/SKHighTemperature.lean:56 (same declaration text).

17. def OAI.SKGap.discreteGap line 60

    Source documentation

    Rayleigh quotient definition of the uniform-site discrete heat-bath gap.

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

    def discreteGap {n : ℕ} (g : Disorder n) : ℝ :=
    …

    Mentions: OAI.SKGap.Disorder

18. def OAI.SKGap.MainStatement line 64

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