BallGrowth.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The neighbourhood inclusions and cardinal growth in Lemma finite:ball-bounds.

def OAI.CycleClique.Construction.outsideBallFinset line 11
theorem OAI.CycleClique.Construction.mem_outsideBallFinset line 16
theorem OAI.CycleClique.Construction.outsideBallFinset_mono line 22
theorem OAI.CycleClique.Construction.outsideBall_step line 29
theorem OAI.CycleClique.Construction.closedNeighborhood_ball_subset line 45
Source documentation
A preceding-ball independent set can acquire outside neighbours only in the next ball. Specified vertices in X can be excluded separately.
```
theorem closedNeighborhood_ball_subset [DecidableEq V] {G : SimpleGraph V} {X A I : Finset V}
    {x : V} {r : ℕ} (hI : I ⊆ outsideBallFinset G X x r)
    (havoid : ∀ v ∈ A, v ∉ closedNeighborhood G I) :
    closedNeighborhood G I ⊆ outsideBallFinset G X x (r + 1) ∪ (X \ A) := by
…
```
Mentions: OAI.CycleClique.Construction.outsideBallFinset, OAI.CycleClique.Construction.closedNeighborhood

theorem OAI.CycleClique.Construction.outsideBall_growth line 62

Source documentation

Additive form of the recursive lower bound, avoiding truncated subtractions when the numerical bound is nonpositive.

theorem outsideBall_growth {G : SimpleGraph V} {k : ℕ} {X A I : Finset V}
    {x : V} {r : ℕ} (hAX : A ⊆ X)
    (hI : I ⊆ outsideBallFinset G X x r)
    (havoid : ∀ v ∈ A, v ∉ closedNeighborhood G I)
    (hexpand : k * I.card + 1 ≤ (closedNeighborhood G I).card) :
    k * I.card + 1 + A.card ≤ (outsideBallFinset G X x (r + 1)).card + X.card := by
…

Mentions: OAI.CycleClique.Construction.outsideBallFinset, OAI.CycleClique.Construction.closedNeighborhood

theorem OAI.CycleClique.Construction.outsideBall_initial_growth line 76

Source documentation

The initial radius-zero bound uses just the singleton expansion and certified nonneighbours in X.

theorem outsideBall_initial_growth {G : SimpleGraph V} {k : ℕ}
    {X A : Finset V} {x : V} (hx : x ∈ X) (hAX : A ⊆ X) (hxA : x ∉ A)
    (hanti : ∀ v ∈ A, ¬ G.Adj x v)
    (hexpand : k + 1 ≤ (closedNeighborhood G {x}).card) :
    k + 1 + A.card ≤ (outsideBallFinset G X x 0).card + X.card := by
…

Mentions: OAI.CycleClique.Construction.closedNeighborhood, OAI.CycleClique.Construction.outsideBallFinset

theorem OAI.CycleClique.Construction.closedNeighborhood_avoids_forbidden line 107
Source documentation
The prohibited short outside paths supply exactly the unavailable vertices needed in the recursive growth estimate.
```
theorem closedNeighborhood_avoids_forbidden {G : SimpleGraph V} {X A I : Finset V}
    {x : V} {r : ℕ} (hx : x ∈ X) (hAX : A ⊆ X) (hxA : x ∉ A)
    (hI : I ⊆ outsideBallFinset G X x r)
    (hforbid : ∀ y ∈ A, ∀ d, 1 ≤ d → d ≤ r + 1 →
      ¬ PositiveOutsidePath G (X : Set V) x y d) :
    ∀ y ∈ A, y ∉ closedNeighborhood G I := by
…
```
Mentions: OAI.CycleClique.Construction.outsideBallFinset, OAI.CycleClique.Construction.PositiveOutsidePath, OAI.CycleClique.Construction.closedNeighborhood