DenseSubgraph.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The dense layer interface

This assembles the minimum-order choice, connectivity, nonbipartiteness, minimum degree, and independent-pair expansion. These are exactly the properties used in the path argument in manuscript Section 3.

theorem OAI.CycleClique.Construction.independent_pair_finset line 14
theorem OAI.CycleClique.Construction.complete_of_indepNum_le_one line 25
theorem OAI.CycleClique.Construction.dense_indepNum_two line 35

theorem OAI.CycleClique.Construction.dense_layer_interface_even line 51

Source documentation

Full even-parameter layer interface.

theorem dense_layer_interface_even {V : Type*} [Fintype V] [DecidableEq V]
    {G : SimpleGraph V} {s : ℕ} (hs : 4 ≤ s)
    (hclique : G.cliqueNum < s) (hInd : IndependenceBound G (2 * s))
    (hexpand : ∀ I : Finset V, G.IsIndepSet (I : Set V) → I.Nonempty →
      2 * s * I.card + 1 ≤ (closedNeighborhood G I).card) (root : V) :
    ∃ i, 1 ≤ i ∧ i ≤ s ∧ ∃ Y : Finset V,
      Y ⊆ distanceLayer G root i ∧ Y.Nonempty ∧
      (G.induce (Y : Set V)).Connected ∧
      ¬ (G.induce (Y : Set V)).IsBipartite ∧ 2 * s ≤ Y.card ∧
      (∀ v : Y, s ≤ ((G.induce (Y : Set V)).neighborSet v).ncard) ∧
      (∀ u v : Y, u ≠ v → ¬ G.Adj u.val v.val →
        2 * s ≤ (closedNeighborhood (G.induce (Y : Set V)) {u, v}).card) := by
…

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

theorem OAI.CycleClique.Construction.dense_layer_interface_odd line 94

Source documentation

Full odd-parameter layer interface.

theorem dense_layer_interface_odd {V : Type*} [Fintype V] [DecidableEq V]
    {G : SimpleGraph V} {s : ℕ} (hs : 4 ≤ s)
    (hclique : G.cliqueNum < s) (hInd : IndependenceBound G (2 * s + 1))
    (hexpand : ∀ I : Finset V, G.IsIndepSet (I : Set V) → I.Nonempty →
      (2 * s + 1) * I.card + 1 ≤ (closedNeighborhood G I).card) (root : V) :
    ∃ i, 1 ≤ i ∧ i ≤ s ∧ ∃ Y : Finset V,
      Y ⊆ distanceLayer G root i ∧ Y.Nonempty ∧
      (G.induce (Y : Set V)).Connected ∧
      ¬ (G.induce (Y : Set V)).IsBipartite ∧ 2 * s + 1 ≤ Y.card ∧
      (∀ v : Y, s ≤ ((G.induce (Y : Set V)).neighborSet v).ncard) ∧
      (∀ u v : Y, u ≠ v → ¬ G.Adj u.val v.val →
        2 * s ≤ (closedNeighborhood (G.induce (Y : Set V)) {u, v}).card) := by
…

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