BallCount.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The uniform maximum-degree exclusion bound for finite graph balls. This treats labelled port graphs too: neighbors forgets multiplicities; loops and multiple edges only decrease the number of distinct vertices.

def OAI.TorsionFreeZeroDivisors.BallCount.ends line 23

Source documentation

Endpoints of walks of exactly k steps.

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

/-- Finite closed combinatorial ball. -/

def OAI.TorsionFreeZeroDivisors.BallCount.ball line 28
Source documentation
Finite closed combinatorial ball.
```
def ball (neighbors : V → Finset V) (x : V) (r : ℕ) : Finset V :=
…
```
theorem OAI.TorsionFreeZeroDivisors.BallCount.card_ends_le line 31
theorem OAI.TorsionFreeZeroDivisors.BallCount.sum_powers_le line 46
Source documentation
A non-asymptotic geometric-sum bound.
```
theorem sum_powers_le (d r : ℕ) (hd : 2 ≤ d) :
    ∑ k ∈ Finset.range (r+1), d^k ≤ 2 * d^r - 1 := by
…
```
theorem OAI.TorsionFreeZeroDivisors.BallCount.card_ball_le line 56
theorem OAI.TorsionFreeZeroDivisors.BallCount.mem_ball_iff line 70
theorem OAI.TorsionFreeZeroDivisors.BallCount.self_mem_ball line 74

theorem OAI.TorsionFreeZeroDivisors.BallCount.port_degree_bound line 80

Source documentation

Forgetting parallel edges is sound for the endpoint bound.

theorem port_degree_bound {T : Type*} (outgoing : V → Finset T) (next : V → T → V)
    (d : ℕ) (hd : ∀ v, (outgoing v).card ≤ d) (v : V) :
    ((outgoing v).image (next v)).card ≤ d :=
…

def OAI.TorsionFreeZeroDivisors.BallCount.graphNeighbors line 86
Source documentation
The ordinary finite neighbor set, with its classical finiteness data fixed.
```
def graphNeighbors [Fintype V] (G : SimpleGraph V) (v : V) : Finset V := by
…
```
theorem OAI.TorsionFreeZeroDivisors.BallCount.mem_graphNeighbors line 91
theorem OAI.TorsionFreeZeroDivisors.BallCount.card_graphNeighbors line 97
theorem OAI.TorsionFreeZeroDivisors.BallCount.mem_ends_of_walk line 104
Source documentation
The finite combinatorial balls contain all walk endpoints, not just paths.
```
theorem mem_ends_of_walk [Fintype V] (G : SimpleGraph V) {a b : V} (p : G.Walk a b) :
    b ∈ ends (graphNeighbors G) a p.length := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BallCount.ends, OAI.TorsionFreeZeroDivisors.BallCount.graphNeighbors
theorem OAI.TorsionFreeZeroDivisors.BallCount.mem_ball_of_walk line 113
theorem OAI.TorsionFreeZeroDivisors.BallCount.far_of_not_mem_ball line 117

theorem OAI.TorsionFreeZeroDivisors.BallCount.matching_bad_card line 127

Source documentation

Removing source and target ports in a bad vertex set discards at most twice its cardinality, since each labelled carrier embeds in the vertex set.

theorem matching_bad_card (f : X ≃ Y) (locX : X → V) (locY : Y → V)
    (hX : Function.Injective locX) (hY : Function.Injective locY) (B : Finset V) :
    (Finset.univ.filter (fun u => locX u ∈ B ∨ locY (f u) ∈ B)).card ≤ 2 * B.card := by
…

theorem OAI.TorsionFreeZeroDivisors.BallCount.admissible_card line 145

Source documentation

A labelled matching has uniformly many choices outside both endpoint balls and outside a prescribed set. This is the quantitative geometric input to the conditioned transposition injection.

theorem admissible_card (f : X ≃ Y) (locX : X → V) (locY : Y → V)
    (hX : Function.Injective locX) (hY : Function.Injective locY)
    (neighbors : V → Finset V) (d : ℕ) (h2 : 2 ≤ d)
    (hd : ∀ v, (neighbors v).card ≤ d) (x y : V) (r : ℕ) (P : Finset X) :
    Fintype.card X - P.card - 4*d^(r+1) ≤
      (Finset.univ.filter (fun u => u ∉ P ∧
        locX u ∉ ball neighbors x r ∪ ball neighbors y r ∧
        locY (f u) ∉ ball neighbors x r ∪ ball neighbors y r)).card := by
…

Mentions: OAI.TorsionFreeZeroDivisors.BallCount.ball