Model.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.CriticalPercolation.BondGraph line 10
Source documentation
An undirected graph with labelled bonds, including loops and parallel bonds.
Also declared: ComparatorChallenges/CriticalPercolation.lean:10 (same declaration text).
```
structure BondGraph (V E : Type*) where
…
```
def OAI.CriticalPercolation.BondGraph.openGraph line 17
Source documentation
The graph of retained bonds. fromEdgeSet discards loops.
Also declared: ComparatorChallenges/CriticalPercolation.lean:17 (same declaration text).
```
def openGraph (ω : Set E) : SimpleGraph V :=
…
```
def OAI.CriticalPercolation.BondGraph.fullGraph line 21
Source documentation
The underlying connectivity graph with every bond retained.
Also declared: ComparatorChallenges/CriticalPercolation.lean:21 (same declaration text).
```
def fullGraph : SimpleGraph V := G.openGraph Set.univ
```
def OAI.CriticalPercolation.BondGraph.LocallyFinite line 24
Source documentation
Local finiteness counts bonds, not just distinct neighbors.
Also declared: ComparatorChallenges/CriticalPercolation.lean:24 (same declaration text).
```
def LocallyFinite : Prop := ∀ v : V, {e : E | v ∈ G.ends e}.Finite
```
structure OAI.CriticalPercolation.BondGraph.Aut line 27
Source documentation
Automorphisms preserve the vertex and bond structure, including multiplicities.
Also declared: ComparatorChallenges/CriticalPercolation.lean:27 (same declaration text).
```
structure Aut where
…
```
def OAI.CriticalPercolation.BondGraph.QuasiTransitive line 33
Source documentation
Finitely many vertex orbits under the full automorphism group.
Also declared: ComparatorChallenges/CriticalPercolation.lean:33 (same declaration text).
```
def QuasiTransitive : Prop :=
…
```
def OAI.CriticalPercolation.BondGraph.cluster line 37
Source documentation
Finite open paths, including the path of length zero, define the open cluster.
Also declared: ComparatorChallenges/CriticalPercolation.lean:37 (same declaration text).
```
def cluster (ω : Set E) (v : V) : Set V := {w | (G.openGraph ω).Reachable v w}
```
def OAI.CriticalPercolation.BondGraph.percolates line 40
Source documentation
The event that at least one open cluster is infinite.
Also declared: ComparatorChallenges/CriticalPercolation.lean:40 (same declaration text).
```
def percolates : Set (Set E) := {ω | ∃ v : V, (G.cluster ω v).Infinite}
```
def OAI.CriticalPercolation.BondGraph.law line 43
Source documentation
Independent retention with parameter p ∈ [0,1] of each labelled bond.
Also declared: ComparatorChallenges/CriticalPercolation.lean:43 (same declaration text).
```
noncomputable def law (_G : BondGraph V E) (p : unitInterval) : Measure (Set E) :=
…
```
Mentions: OAI.CriticalPercolation.BondGraph
def OAI.CriticalPercolation.BondGraph.criticalProbability line 47
Source documentation
The infimum of parameters with positive probability of an infinite cluster.
Also declared: ComparatorChallenges/CriticalPercolation.lean:47 (same declaration text).
```
noncomputable def criticalProbability : unitInterval :=
…
```