LayerMinimal.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Expansion inside a minimum-order dense layer subgraph

These are the independent-set deletion calculations in manuscript Proposition clq:layer-interface. Both parity cases are stated: for an even parameter the order inequality is weak and minimality is strict; for an odd parameter the order inequality is strict and minimality weak.

theorem OAI.CycleClique.Construction.independenceBound_indepNum line 15
theorem OAI.CycleClique.Construction.indepNum_le_of_independenceBound line 18
theorem OAI.CycleClique.Construction.outside_indepNum_bound line 24

theorem OAI.CycleClique.Construction.minimal_dense_expansion_even line 33

Source documentation

Even-parameter local minimality gives strict neighbourhood expansion unless the neighbourhood is the entire graph.

theorem minimal_dense_expansion_even {V : Type*} [Fintype V]
    {G : SimpleGraph V} {s : ℕ}
    (hdense : s * G.indepNum ≤ Fintype.card V)
    (hminimal : ∀ Y : Finset V, Y.Nonempty → Y.card < Fintype.card V →
      Y.card < s * (G.induce (Y : Set V)).indepNum)
    (I : Finset V) (hI : G.IsIndepSet (I : Set V)) (hne : I.Nonempty) :
    s * I.card ≤ (closedNeighborhood G I).card ∧
      ((closedNeighborhood G I).card < Fintype.card V →
        s * I.card < (closedNeighborhood G I).card) := by
…

Mentions: OAI.CycleClique.Construction.closedNeighborhood

theorem OAI.CycleClique.Construction.minimal_dense_expansion_odd line 69

Source documentation

Odd-parameter local minimality gives strict neighbourhood expansion for every nonempty independent set.

theorem minimal_dense_expansion_odd {V : Type*} [Fintype V]
    {G : SimpleGraph V} {s : ℕ}
    (hdense : s * G.indepNum < Fintype.card V)
    (hminimal : ∀ Y : Finset V, Y.Nonempty → Y.card < Fintype.card V →
      Y.card ≤ s * (G.induce (Y : Set V)).indepNum)
    (I : Finset V) (hI : G.IsIndepSet (I : Set V)) (hne : I.Nonempty) :
    s * I.card < (closedNeighborhood G I).card := by
…

Mentions: OAI.CycleClique.Construction.closedNeighborhood