OAI/Probability/CriticalZ3/Subunit.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BlockPercolation.active line 13
2. def OAI.BlockPercolation.Bad line 16
3. def OAI.BlockPercolation.Adj line 19
4. def OAI.BlockPercolation.cluster line 22
5. theorem OAI.BlockPercolation.root_mem_iff line 25
6. theorem OAI.BlockPercolation.cluster_active line 29
7. theorem OAI.BlockPercolation.outside_bad line 36
8. theorem OAI.BlockPercolation.bad_determined line 42
9. theorem OAI.BlockPercolation.measurableSet_bad line 52
10. theorem OAI.BlockPercolation.single_closed_probability line 56
11. theorem OAI.BlockPercolation.bad_probability_le line 69
12. theorem OAI.BlockPercolation.survival line 87

    Source documentation

    Peierls survival for independent finite blocks of at most two bits.

    theorem survival (p : Set.Icc (0 : ℝ) 1) (J : Point → Finset E)
        (hJ : Pairwise (fun u v => Disjoint (J u) (J v))) (hcard : ∀ v, (J v).card ≤ 2)
        (hp : 2*(1-(p : ℝ)) ≤ CriticalScales.contourError)
        (A : Set (E → Bool))
        (hA : ∀ ω, (cluster J ω).Infinite → ω ∈ A) :
        0 < ProductCylinder.law (fun _ : E => p) A := by
    …

    Mentions: OAI.CriticalScales.contourError, OAI.BlockPercolation.cluster, OAI.ProductCylinder.law

13. def OAI.CriticalZ3.planarEmbed line 128

    Source documentation

    The planar sublattice used only for the elementary strict upper threshold.

    def planarEmbed (v : Point) : Vertex := ![v.1,v.2,0]

    Mentions: OAI.CriticalZ3.Vertex

14. theorem OAI.CriticalZ3.planarEmbed_injective line 130
15. theorem OAI.CriticalZ3.planarEmbed_zero line 136
16. def OAI.CriticalZ3.planarSiteBlock line 139
17. def OAI.CriticalZ3.planarBondBlock line 141
18. theorem OAI.CriticalZ3.planarSiteBlock_disjoint line 143
19. theorem OAI.CriticalZ3.planarBondBlock_disjoint line 148
20. theorem OAI.CriticalZ3.planarSiteBlock_card line 157
21. theorem OAI.CriticalZ3.planarBondBlock_card line 158
22. theorem OAI.CriticalZ3.planar_neighbor line 161
23. theorem OAI.CriticalZ3.planar_site_open line 173
24. theorem OAI.CriticalZ3.planar_bond_open line 179
25. theorem OAI.CriticalZ3.planar_bond_infinite line 197
26. theorem OAI.CriticalZ3.planar_site_infinite line 206
27. def OAI.CriticalZ3.subunitParameter line 216
28. theorem OAI.CriticalZ3.subunitParameter_lt_one line 222
29. theorem OAI.CriticalZ3.subunit_bond_positive line 226
30. theorem OAI.CriticalZ3.subunit_site_positive line 234
31. theorem OAI.CriticalZ3.bondCritical_lt_one line 242
32. theorem OAI.CriticalZ3.siteCritical_lt_one line 247