LayerSelection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Choosing the minimum dense induced subgraph in a layer

The two selection lemmas make the minimum-order choice in manuscript Proposition clq:layer-interface and supply exactly the local minimality premises used by the expansion and connectivity arguments.

theorem OAI.CycleClique.Construction.indepNum_le_of_induced_injection line 14
theorem OAI.CycleClique.Construction.indepNum_eq_of_iso line 27
def OAI.CycleClique.Construction.nestedInduceIso line 34

theorem OAI.CycleClique.Construction.exists_minimal_dense_even line 55

Source documentation

The minimum-order weakly dense subgraph of a layer (even k).

theorem exists_minimal_dense_even {V : Type*} [Fintype V] {G : SimpleGraph V}
    {s : ℕ} (D : Finset V) (hD : D.Nonempty)
    (hdense : s * (G.induce (D : Set V)).indepNum ≤ D.card) :
    ∃ Y : Finset V, Y ⊆ D ∧ Y.Nonempty ∧
      s * (G.induce (Y : Set V)).indepNum ≤ Y.card ∧
      ∀ Z : Finset Y, Z.Nonempty → Z.card < Y.card →
        Z.card < s * ((G.induce (Y : Set V)).induce (Z : Set Y)).indepNum := by
…

theorem OAI.CycleClique.Construction.exists_minimal_dense_odd line 90

Source documentation

The minimum-order strictly dense subgraph of a layer (odd k).

theorem exists_minimal_dense_odd {V : Type*} [Fintype V] {G : SimpleGraph V}
    {s : ℕ} (D : Finset V) (hD : D.Nonempty)
    (hdense : s * (G.induce (D : Set V)).indepNum < D.card) :
    ∃ Y : Finset V, Y ⊆ D ∧ Y.Nonempty ∧
      s * (G.induce (Y : Set V)).indepNum < Y.card ∧
      ∀ Z : Finset Y, Z.Nonempty → Z.card < Y.card →
        Z.card ≤ s * ((G.induce (Y : Set V)).induce (Z : Set Y)).indepNum := by
…