Peierls.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PlanarBoundary.blocked line 17

theorem OAI.PlanarBoundary.blocked_bound line 21

Source documentation

Matching and endpoint union bound; the bad vertices may be arbitrarily dependent.

theorem blocked_bound {n : ℕ} (Bad : Point → Set Ω) (c : Code n) (hc : Valid c)
    {f : ℝ} (hf0 : 0 < f) (hf1 : 2*f ≤ 1)
    (hbad : ∀ s : Finset Point, μ.real {ω | ∀ v ∈ s, ω ∈ Bad v} ≤ f^s.card) :
    μ.real (blocked Bad c) ≤ (2*f)^((n : ℝ)/7) := by
…

Mentions: OAI.PlanarBoundary.Point, OAI.PlanarBoundary.Code, OAI.PlanarBoundary.Valid, OAI.PlanarBoundary.blocked

def OAI.PlanarBoundary.candidate line 67
Source documentation
Codes arising from actual boundaries are the only candidates needed.
```
def candidate {n : ℕ} (Bad : Point → Set Ω) (c : {c : Code n // Valid c}) : Set Ω :=
…
```
Mentions: OAI.PlanarBoundary.Point, OAI.PlanarBoundary.Code, OAI.PlanarBoundary.Valid
theorem OAI.PlanarBoundary.candidates_bound line 70

theorem OAI.PlanarBoundary.union_bound line 86

Source documentation

A summable real upper bound for countably many events bounds their union.

theorem union_bound (A : ℕ → Set Ω) (g : ℕ → ℝ) (hg0 : ∀ n, 0 ≤ g n)
    (hg : Summable g) (hA : ∀ n, μ.real (A n) ≤ g n) :
    μ.real (⋃ n, A n) ≤ ∑' n, g n := by
…

theorem OAI.PlanarBoundary.encoded_budget_hasSum line 97
Source documentation
Exact numerical budget for the benign overcount of encoded trails.
```
theorem encoded_budget_hasSum :
    HasSum (fun n : ℕ => 4*(n : ℝ)*4^n*(2*CriticalScales.contourError)^((n : ℝ)/7)) (25/144 : ℝ) := by
…
```
Mentions: OAI.CriticalScales.contourError

theorem OAI.PlanarBoundary.finite_good_subset line 113

Source documentation

The main contour inclusion, without conditioning on a random boundary.

theorem finite_good_subset (Good : Ω → Set Point) (Bad : Point → Set Ω)
    (houtside : ∀ ω, (Good ω).Finite → ∀ x ∈ Good ω, ∀ d : Direction,
      x+outward d ∉ Good ω → ω ∈ Bad (x+outward d)) :
    {ω | (Good ω).Finite ∧ (0,0) ∈ Good ω} ⊆
      ⋃ n, ⋃ c : {c : Code n // Valid c}, candidate Bad c := by
…

Mentions: OAI.PlanarBoundary.Point, OAI.PlanarBoundary.Direction, OAI.PlanarBoundary.outward, OAI.PlanarBoundary.Code, OAI.PlanarBoundary.Valid, OAI.PlanarBoundary.candidate

theorem OAI.PlanarBoundary.finite_good_bound line 131