Boundaries of hypergraphs

A signal may have many consumers, but a separator pays for its value only once. Its native incidence object is therefore a hyperedge. Hypergraph cut cardinality is symmetric and submodular, so it is a connectivity function even when the hyperedges have unbounded size.

@[reducible, inline]

abbrev Complexity.Frontier.Hypergraph (V : Type u_4) (Λ : Type u_5) : Type (max u_5 u_4)

A hypergraph, with named hyperedges and no restriction on their size.

Equations

• Complexity.Frontier.Hypergraph V Λ = (Λ → Set V)

def Complexity.Frontier.Hypergraph.cut {V : Type u_1} {Λ : Type u_3} (H : Hypergraph V Λ) (X : Set V) : Set Λ

Hyperedges meeting both sides of a vertex separator.

Equations

• H.cut X = {e : Λ | (H e ∩ X).Nonempty ∧ (H e \ X).Nonempty}

@[simp]

theorem Complexity.Frontier.Hypergraph.cut_compl {V : Type u_1} {Λ : Type u_3} (H : Hypergraph V Λ) (X : Set V) : H.cut Xᶜ = H.cut X

@[simp]

theorem Complexity.Frontier.Hypergraph.cut_empty {V : Type u_1} {Λ : Type u_3} (H : Hypergraph V Λ) : H.cut ∅ = ∅

@[simp]

theorem Complexity.Frontier.Hypergraph.cut_univ {V : Type u_1} {Λ : Type u_3} (H : Hypergraph V Λ) : H.cut Set.univ = ∅

theorem Complexity.Frontier.Hypergraph.cut_union_inter_subset {V : Type u_1} {Λ : Type u_3} (H : Hypergraph V Λ) (X Y : Set V) : H.cut (X ∩ Y) ∪ H.cut (X ∪ Y) ⊆ H.cut X ∪ H.cut Y

theorem Complexity.Frontier.Hypergraph.cut_inter_union_subset {V : Type u_1} {Λ : Type u_3} (H : Hypergraph V Λ) (X Y : Set V) : H.cut (X ∩ Y) ∩ H.cut (X ∪ Y) ⊆ H.cut X ∩ H.cut Y

theorem Complexity.Frontier.Hypergraph.ncard_cut_submodular {V : Type u_1} {Λ : Type u_3} [Finite Λ] (H : Hypergraph V Λ) (X Y : Set V) : (H.cut (X ∩ Y)).ncard + (H.cut (X ∪ Y)).ncard ≤ (H.cut X).ncard + (H.cut Y).ncard

Hypergraph boundary size is submodular.

def Complexity.Frontier.Multigraph.signalHypergraph {V : Type u_1} {E : Type u_2} {Λ : Type u_3} (G : Multigraph V E) (label : E → Λ) : Hypergraph V Λ

Contract the endpoints carrying the same signal into a native hyperedge.

Equations

• G.signalHypergraph label s = {v : V | ∃ (e : E), label e = s ∧ G.Incident v e}

theorem Complexity.Frontier.Multigraph.image_cut_subset_hypergraph_cut {V : Type u_1} {E : Type u_2} {Λ : Type u_3} (G : Multigraph V E) (label : E → Λ) (X : Set V) : label '' G.cut X ⊆ (G.signalHypergraph label).cut X

Every crossing labelled edge gives a crossing signal hyperedge. The converse requires the occurrences of a label to be connected; it is false for arbitrary labellings.

def Complexity.Frontier.Multigraph.labelGraph {V : Type u_1} {E : Type u_2} {Λ : Type u_3} (G : Multigraph V E) (label : E → Λ) (s : Λ) : Multigraph V { e : E // label e = s }

The graph consisting of the edges with one chosen label.

Equations

• G.labelGraph label s = { src := fun (e : { e : E // label e = s }) => G.src ↑e, tgt := fun (e : { e : E // label e = s }) => G.tgt ↑e }

theorem Complexity.Frontier.Multigraph.image_cut_eq_hypergraph_cut {V : Type u_1} {E : Type u_2} {Λ : Type u_3} (G : Multigraph V E) (label : E → Λ) (hconn : ∀ (s : Λ), ∀ u ∈ G.signalHypergraph label s, ∀ v ∈ G.signalHypergraph label s, Relation.ReflTransGen (G.labelGraph label s).Adj u v) (X : Set V) : label '' G.cut X = (G.signalHypergraph label).cut X

A connected occurrence graph makes the native hypergraph boundary exact.