OAI/Probability/CriticalZ3/LatticeGraph.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalZ3.Incidence line 13

   Source documentation

   An unoriented nearest-neighbor bond, in its unique positive-axis indexing.

   def Incidence (e : Bond) (x y : Vertex) : Prop :=
   …

   Mentions: OAI.CriticalZ3.Bond, OAI.CriticalZ3.Vertex

2. theorem OAI.CriticalZ3.step_ne line 16
3. theorem OAI.CriticalZ3.incidence_symm line 21
4. theorem OAI.CriticalZ3.incidence_ne line 24
5. theorem OAI.CriticalZ3.incidence_neighbor line 29
6. structure OAI.CriticalZ3.LatticeGraph line 35
7. abbrev OAI.CriticalZ3.LatticeGraph.Node line 44
8. def OAI.CriticalZ3.LatticeGraph.graph line 46
9. def OAI.CriticalZ3.LatticeGraph.hypergraph line 51
10. def OAI.CriticalZ3.LatticeGraph.BondAdj line 54
11. def OAI.CriticalZ3.LatticeGraph.BondConn line 57
12. def OAI.CriticalZ3.LatticeGraph.SiteConn line 60
13. def OAI.CriticalZ3.LatticeGraph.BondMeets line 63
14. def OAI.CriticalZ3.LatticeGraph.SiteMeets line 66
15. theorem OAI.CriticalZ3.LatticeGraph.bondAdj_open line 69
16. theorem OAI.CriticalZ3.LatticeGraph.bondConn_global line 76
17. theorem OAI.CriticalZ3.LatticeGraph.siteConn_global line 80
18. theorem OAI.CriticalZ3.LatticeGraph.bondAdj_determined line 87
19. theorem OAI.CriticalZ3.LatticeGraph.bondConn_determined line 94
20. theorem OAI.CriticalZ3.LatticeGraph.siteConn_determined line 101
21. theorem OAI.CriticalZ3.LatticeGraph.bondMeets_determined line 108
22. theorem OAI.CriticalZ3.LatticeGraph.siteMeets_determined line 113
23. theorem OAI.CriticalZ3.LatticeGraph.bondConn_iff_hypergraph line 118
24. theorem OAI.CriticalZ3.LatticeGraph.bondMeets_probability line 145

    Source documentation

    Pulling the actual bond connection event down to its finite bit set.

    theorem bondMeets_probability (p : Bond → Set.Icc (0 : ℝ) 1)
        (o : G.Node) (T : Set Vertex) :
        (ProductCylinder.law p).real {ω | G.BondMeets ω o T} =
          HyperedgeComparison.eventProb (fun e : G.edges => p e.1)
            (fun ω => HyperedgeComparison.Meets G.hypergraph ω ∅ o {y | y.1 ∈ T}) := by
    …

    Mentions: OAI.CriticalZ3.Bond, OAI.CriticalZ3.Vertex, OAI.ProductCylinder.law, OAI.HyperedgeComparison.eventProb, OAI.HyperedgeComparison.Meets

25. theorem OAI.CriticalZ3.LatticeGraph.siteMeets_probability line 163
26. theorem OAI.CriticalZ3.LatticeGraph.bondObservable_probability line 179

    Source documentation

    Any observable of the finite graph's connections is a finite cylinder.

    theorem bondObservable_probability (p : Bond → Set.Icc (0 : ℝ) 1)
        (φ : (G.Node → Set Vertex → Prop) → Prop) :
        (ProductCylinder.law p).real {ω | φ (G.BondMeets ω)} =
          HyperedgeComparison.eventProb (fun e : G.edges => p e.1)
            (fun ω => φ (fun o T => HyperedgeComparison.Meets G.hypergraph ω ∅ o {y | y.1 ∈ T})) := by
    …

    Mentions: OAI.CriticalZ3.Bond, OAI.CriticalZ3.Vertex, OAI.ProductCylinder.law, OAI.HyperedgeComparison.eventProb, OAI.HyperedgeComparison.Meets

27. theorem OAI.CriticalZ3.LatticeGraph.siteObservable_probability line 205
28. theorem OAI.CriticalZ3.LatticeGraph.bond_failure_comparison line 232

    Source documentation

    The comparison is now attached to actual finite lattice bond paths and arbitrary independent laws on the entire lattice, not an assumed interface.

    theorem bond_failure_comparison (p : Bond → Set.Icc (0 : ℝ) 1)
        (o : G.Node) (A T : Set Vertex) {b : ℝ} (hb0 : 0 ≤ b)
        (hb : ∀ a : G.Node, a.1 ∈ A →
          1-b ≤ (ProductCylinder.law p).real {ω | G.BondMeets ω a T}) :
        (ProductCylinder.law p).real {ω | G.BondMeets ω o A ∧ ¬G.BondMeets ω o T} ≤ b := by
    …

    Mentions: OAI.CriticalZ3.Bond, OAI.CriticalZ3.Vertex, OAI.ProductCylinder.law

29. theorem OAI.CriticalZ3.LatticeGraph.site_failure_comparison line 242