LayerStructure.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Connectivity and nonbipartiteness of a minimum dense subgraph

These are the structural consequences of the minimum-order choice in manuscript Proposition clq:layer-interface.

theorem OAI.CycleClique.Construction.indepNum_induce_add_le line 16

Source documentation

Independence numbers add across disjoint anticomplete vertex sets.

theorem indepNum_induce_add_le {V : Type*} [Fintype V] {G : SimpleGraph V}
    (A B : Finset V) (hdis : Disjoint A B)
    (hanti : ∀ x ∈ A, ∀ y ∈ B, ¬ G.Adj x y) :
    (G.induce (A : Set V)).indepNum + (G.induce (B : Set V)).indepNum ≤ G.indepNum := by
…

structure OAI.CycleClique.Construction.DisconnectedPartition line 56
theorem OAI.CycleClique.Construction.disconnected_partition line 66
theorem OAI.CycleClique.Construction.DisconnectedPartition.card line 86

theorem OAI.CycleClique.Construction.minimal_dense_connected_even line 94

Source documentation

A minimum-order induced graph satisfying the even-parameter density inequality is connected.

theorem minimal_dense_connected_even {V : Type*} [Fintype V] [Nonempty 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) : G.Connected := by
…

theorem OAI.CycleClique.Construction.minimal_dense_connected_odd line 114

Source documentation

A minimum-order induced graph satisfying the odd-parameter strict density inequality is connected.

theorem minimal_dense_connected_odd {V : Type*} [Fintype V] [Nonempty 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) : G.Connected := by
…

theorem OAI.CycleClique.Construction.bipartite_order_bound line 134
Source documentation
Every bipartite graph has an independent set containing at least half its vertices.
```
theorem bipartite_order_bound {V : Type*} [Fintype V] {G : SimpleGraph V}
    (hbip : G.IsBipartite) : Fintype.card V ≤ 2 * G.indepNum := by
…
```

theorem OAI.CycleClique.Construction.dense_nonbipartite line 156

Source documentation

The dense layer subgraph is nonbipartite.

theorem dense_nonbipartite {V : Type*} [Fintype V] [Nonempty V]
    {G : SimpleGraph V} {s : ℕ} (hs : 3 ≤ s)
    (hdense : s * G.indepNum ≤ Fintype.card V) : ¬ G.IsBipartite := by
…

theorem OAI.CycleClique.Construction.closedNeighborhood_singleton_card line 168
Source documentation
Closed singleton neighbourhoods have one more vertex than the degree.
```
theorem closedNeighborhood_singleton_card {V : Type*} [Fintype V]
    (G : SimpleGraph V) (v : V) :
    (closedNeighborhood G {v}).card = (G.neighborSet v).ncard + 1 := by
…
```
Mentions: OAI.CycleClique.Construction.closedNeighborhood

theorem OAI.CycleClique.Construction.dense_expansion_degree line 181

Source documentation

The singleton consequence of the dense-minimal expansion bound gives the minimum degree needed by the coloured-path argument.

theorem dense_expansion_degree {V : Type*} [Fintype V] {G : SimpleGraph V}
    {s : ℕ} (_hs : 1 ≤ s) (horder : 2 * s ≤ Fintype.card V)
    (hstrict : ∀ v : V, (closedNeighborhood G {v}).card < Fintype.card V →
      s < (closedNeighborhood G {v}).card) :
    ∀ v, s ≤ (G.neighborSet v).ncard := by
…

Mentions: OAI.CycleClique.Construction.closedNeighborhood