BoundedGeometry.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Uniformly bounded degree gives uniformly finite graph balls

The elementary bounded-geometry argument used in §3 of the coarse Novikov manuscript. Finite neighbor lists are supplied for an arbitrary graph; no finiteness assumption is made about the whole vertex set. The bound (degreeBound + 1)^radius is sufficient for the application.

def OAI.CoarseAssembly.walkBall line 24

Source documentation

A finite over-approximation of vertices reached in at most r edges.

def walkBall (neighbors : V → Finset V) (x : V) : ℕ → Finset V
  | 0 => {x}
  | r + 1 => walkBall neighbors x r ∪ (walkBall neighbors x r).biUnion neighbors

theorem OAI.CoarseAssembly.mem_walkBall_zero line 28
theorem OAI.CoarseAssembly.walkBall_mono_step line 31
theorem OAI.CoarseAssembly.walkBall_mono line 35

theorem OAI.CoarseAssembly.card_walkBall_le line 42

Source documentation

A uniform degree bound bounds every finite combinatorial ball.

theorem card_walkBall_le (neighbors : V → Finset V) (d : ℕ)
    (hd : ∀ v, (neighbors v).card ≤ d) (x : V) (r : ℕ) :
    (walkBall neighbors x r).card ≤ (d + 1) ^ r := by
…

Mentions: OAI.CoarseAssembly.walkBall

theorem OAI.CoarseAssembly.endpoint_mem_walkBall line 62

Source documentation

Each walk endpoint belongs to the finite ball of its length.

theorem endpoint_mem_walkBall (neighbors : V → Finset V)
    (hN : ∀ u v, G.Adj u v → v ∈ neighbors u) {x y : V} (p : G.Walk x y) :
    y ∈ walkBall neighbors x p.length := by
…

Mentions: OAI.CoarseAssembly.walkBall

theorem OAI.CoarseAssembly.finite_edist_ball line 72

Source documentation

Closed graph balls are finite, uniformly in the center.

theorem finite_edist_ball (neighbors : V → Finset V)
    (hN : ∀ u v, G.Adj u v → v ∈ neighbors u) (x : V) (r : ℕ) :
    {y | G.edist x y ≤ (r : ℕ∞)}.Finite := by
…

theorem OAI.CoarseAssembly.ncard_edist_ball_le line 82

Source documentation

An explicit cardinal bound independent of the center.

theorem ncard_edist_ball_le (neighbors : V → Finset V) (d : ℕ)
    (hN : ∀ u v, G.Adj u v → v ∈ neighbors u)
    (hd : ∀ v, (neighbors v).card ≤ d) (x : V) (r : ℕ) :
    Set.ncard {y | G.edist x y ≤ (r : ℕ∞)} ≤ (d + 1) ^ r := by
…