ShellProbability.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.CriticalZ3.LatticeGraph.shell_blocking_lower line 13
theorem OAI.CriticalZ3.LatticeGraph.measurableSet_shell_blocked line 59

theorem OAI.CriticalZ3.LatticeGraph.exists_shell line 84

Source documentation

Deterministic shell selection for the finite graph in bond and site percolation.

theorem exists_shell (p : m.Bit → Set.Icc (0 : ℝ) 1)
    (B : Box) (o : G.Node) (q : Set.Icc (0 : ℝ) 1) {p₀ : ℝ}
    (hq : (q : ℝ) ≤ p₀) (hp₀ : p₀ < 1) (L a R : ℕ) (haR : a < R)
    (ho : ¬(B.expand R).Contains o.1)
    (hp : ∀ j ∈ Finset.Ico a R, ∀ y, (B.expand j).Exterior y →
      p ((B.expand j).entryBit m y) = q) :
    ∃ j ∈ Finset.Ico a R, (ProductCylinder.law p).real
      {ω | G.Meets m ω o {x | B.Contains x} ∧ (G.entrants m (B.expand j) ω o).card < L} ≤
      1/((1-p₀)^L*(R-a : ℕ)) := by
…

Mentions: OAI.CriticalZ3.Box, OAI.ProductCylinder.law

theorem OAI.FiniteAssociation.indicator_monotone line 138
theorem OAI.FiniteAssociation.prob_and_increasing line 146
theorem OAI.ProductCylinder.probability_congr_parameters line 161
theorem OAI.ProductCylinder.determinedBy_mono line 172
theorem OAI.ProductCylinder.increasing_and line 176
theorem OAI.ProductCylinder.seed_failure_bound line 194
Source documentation
The open-seed Harris estimate, with a separate increasing connecting event.
```
theorem seed_failure_bound (J : Finset E) (p : E → Set.Icc (0 : ℝ) 1)
    (O A C : Set (E → Bool))
    (hO : DeterminedBy (F := Prop) J (fun ω => ω ∈ O))
…
```
Mentions: OAI.ProductCylinder.DeterminedBy
theorem OAI.InfiniteConditioning.allValue_true_monotone line 216
theorem OAI.InfiniteConditioning.measurableSet_conditional_test line 222
theorem OAI.CriticalZ3.LatticeGraph.conn_mono line 234
theorem OAI.CriticalZ3.LatticeGraph.meets_mono line 252
def OAI.CriticalZ3.LatticeGraph.goodRelays line 256
theorem OAI.CriticalZ3.LatticeGraph.goodRelays_determined line 260
theorem OAI.CriticalZ3.LatticeGraph.random_relay_failure line 266