DistanceLayers.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Distance layers and independent parity unions

Distance layers are restricted to the root's connected component. Vertices in different layers of the same parity are anticomplete, so maximum independent sets chosen there can be combined.

def OAI.CycleClique.Construction.independentOn line 16
theorem OAI.CycleClique.Construction.independentOn_subset line 22
theorem OAI.CycleClique.Construction.independentOn_independent line 29
theorem OAI.CycleClique.Construction.independentOn_card line 38
def OAI.CycleClique.Construction.distanceLayer line 46
Source documentation
The exact-distance layer within the root component.
```
noncomputable def distanceLayer {V : Type*} [Fintype V]
    (G : SimpleGraph V) (root : V) (j : ℕ) : Finset V := by
…
```
theorem OAI.CycleClique.Construction.mem_distanceLayer line 51
theorem OAI.CycleClique.Construction.distanceLayer_zero line 57
theorem OAI.CycleClique.Construction.distanceLayers_disjoint line 70

theorem OAI.CycleClique.Construction.same_parity_layers_anticomplete line 79

Source documentation

Distinct layers of one parity have no edges between them.

theorem same_parity_layers_anticomplete {V : Type*} [Fintype V]
    {G : SimpleGraph V} {root : V} {i j : ℕ} (hij : i ≠ j) (hparity : i % 2 = j % 2)
    {x y : V} (hx : x ∈ distanceLayer G root i) (hy : y ∈ distanceLayer G root j) :
    ¬ G.Adj x y := by
…

Mentions: OAI.CycleClique.Construction.distanceLayer

theorem OAI.CycleClique.Construction.distanceLayer_neighbor_le line 90

Source documentation

Neighbours of a vertex in layer i belong to one of the first i + 2 layers.

theorem distanceLayer_neighbor_le {V : Type*} [Fintype V]
    {G : SimpleGraph V} {root x y : V} {i : ℕ}
    (hx : x ∈ distanceLayer G root i) (hxy : G.Adj x y) :
    ∃ j ≤ i + 1, y ∈ distanceLayer G root j := by
…

Mentions: OAI.CycleClique.Construction.distanceLayer

theorem OAI.CycleClique.Construction.parity_layer_independence_bound line 102

Source documentation

Alternating maximum-independent-set sums are at most the ambient independence bound.

theorem parity_layer_independence_bound {V : Type*} [Fintype V]
    {G : SimpleGraph V} {k : ℕ} (hbound : IndependenceBound G k) (root : V) (i : ℕ) :
    ∑ j ∈ (Finset.range (i + 1)).filter (fun j => j % 2 = i % 2),
      (G.induce (distanceLayer G root j : Set V)).indepNum ≤ k := by
…

Mentions: OAI.CycleClique.Construction.IndependenceBound, OAI.CycleClique.Construction.distanceLayer