OrientedProbability.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite-dependent high-density bound in crossings.tex:cr:oriented-paths. The tests need not be stationary.

def OAI.PlanarFPP.SeparatedGoodIndependent line 16
Also declared: OAI/Probability/FirstPassage/OrientedProbability.lean:13 (same declaration text).
theorem OAI.PlanarFPP.independent_complement_inter line 21
Also declared: OAI/Probability/FirstPassage/OrientedProbability.lean:18 (same declaration text).
theorem OAI.PlanarFPP.contour_bad_probability line 34
Source documentation
Probability of all forced-bad sites on one fixed loop. The exponent uses an integer threshold, avoiding a rounding loss in m/[8(2k+1)^2].
Also declared: OAI/Probability/FirstPassage/OrientedProbability.lean:29 (same declaration text).
```
theorem contour_bad_probability {m : ℕ} (c : SquareLoop m)
    (hc : c.NoRepeatedSides) (G : Vertex → Set Ω) (k : ℕ)
    (hind : SeparatedGoodIndependent P G k)
    (q : ℝ≥0∞) (hq : q ≤ 1)
    (hbad : ∀ v, P (G v)ᶜ ≤ q^(8*(2*k+1)^2)) :
    P {ω | ∀ v ∈ c.badSites, ω ∉ G v} ≤ q^m := by
…
```
Mentions: OAI.PlanarFPP.SquareLoop, OAI.PlanarFPP.Vertex, OAI.PlanarFPP.SeparatedGoodIndependent
theorem OAI.PlanarFPP.enclosingLoop_card_geometric line 58
Also declared: OAI/Probability/FirstPassage/OrientedProbability.lean:53 (same declaration text).