BallSeparation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Outside paths and separated neighbourhood balls

This is manuscript Lemma path:separation. The boundary graph deletes edges with both ends in X, so shortening a walk cannot introduce a direct edge between its two endpoints in X.

def OAI.CycleClique.Construction.boundaryGraph line 18
Source documentation
Delete precisely the edges with both ends in the excluded vertex set.
```
def boundaryGraph (G : SimpleGraph V) (X : Set V) : SimpleGraph V where
…
```
def OAI.CycleClique.Construction.PositiveOutsidePath line 25
Source documentation
A positive-parameter outside path: exactly d internal vertices, all outside X. The boundary graph excludes the parameter-zero edge.
```
def PositiveOutsidePath (G : SimpleGraph V) (X : Set V) (x y : V) (d : ℕ) : Prop :=
…
```
def OAI.CycleClique.Construction.OutsideBall line 32
Source documentation
The ball reached by at most r edges after the first outside neighbour of x, with all subsequent vertices outside X.
```
def OutsideBall (G : SimpleGraph V) (X : Set V) (x : V) (r : ℕ) : Set V :=
…
```
theorem OAI.CycleClique.Construction.OutsideBall.mono line 36
theorem OAI.CycleClique.Construction.outsideBall_zero line 41
theorem OAI.CycleClique.Construction.outside_path_of_walk line 59

theorem OAI.CycleClique.Construction.outside_balls_separated line 80

Source documentation

Forbidding the specified positive outside paths separates two balls both as vertex sets and by the absence of edges between them.

theorem outside_balls_separated {G : SimpleGraph V} {X : Set V} {x y : V}
    (hx : x ∈ X) (hy : y ∈ X) (hxy : x ≠ y) {r s : ℕ}
    (hforbid : ∀ d, 1 ≤ d → d ≤ r + s + 2 → ¬ PositiveOutsidePath G X x y d) :
    Disjoint (OutsideBall G X x r) (OutsideBall G X y s) ∧
    ∀ u ∈ OutsideBall G X x r, ∀ v ∈ OutsideBall G X y s, ¬ G.Adj u v := by
…

Mentions: OAI.CycleClique.Construction.PositiveOutsidePath, OAI.CycleClique.Construction.OutsideBall

theorem OAI.CycleClique.Construction.singleton_outside_ball_separated line 119

Source documentation

The singleton/ball case of the same separation principle.

theorem singleton_outside_ball_separated {G : SimpleGraph V} {X : Set V} {x y : V}
    (hx : x ∈ X) (hy : y ∈ X) (hxy : x ≠ y) {r : ℕ}
    (hforbid : ∀ d, 1 ≤ d → d ≤ r + 1 → ¬ PositiveOutsidePath G X x y d) :
    ∀ v ∈ OutsideBall G X x r, ¬ G.Adj v y := by
…

Mentions: OAI.CycleClique.Construction.PositiveOutsidePath, OAI.CycleClique.Construction.OutsideBall