Counting multigraph boundaries

Parallel edges are distinct records throughout. The simple support supplies distances; the multigraph supplies degrees, crossing counts, and the core density estimate.

def Complexity.Frontier.Multigraph.support {V : Type u_1} {E : Type u_2} (G : Multigraph V E) : SimpleGraph V

The simple support of a multigraph, with loops discarded.

Equations

• G.support = SimpleGraph.fromRel G.Adj

theorem Complexity.Frontier.Multigraph.support_adj {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {u v : V} : G.support.Adj u v ↔ u ≠ v ∧ G.Adj u v

theorem Complexity.Frontier.Multigraph.support_src_tgt {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (hl : G.Loopless) (e : E) : G.support.Adj (G.src e) (G.tgt e)

theorem Complexity.Frontier.Multigraph.support_degree_le {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] [G.support.LocallyFinite] (v : V) : G.support.degree v ≤ (G.edgesAt v).ncard

Distinct neighbours inject into incident edges.

noncomputable def Complexity.Frontier.Multigraph.crossingFinset {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Fintype E] (S : Finset V) : Finset E

A finite cut, retaining edge multiplicity.

Equations

• G.crossingFinset S = {e : E | ¬(G.src e ∈ S ↔ G.tgt e ∈ S)}

@[simp]

theorem Complexity.Frontier.Multigraph.mem_crossingFinset {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Fintype E] {S : Finset V} {e : E} : e ∈ G.crossingFinset S ↔ ¬(G.src e ∈ S ↔ G.tgt e ∈ S)

theorem Complexity.Frontier.Multigraph.card_crossingFinset {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Fintype E] (S : Finset V) : (G.crossingFinset S).card = (G.cut ↑S).ncard

theorem Complexity.Frontier.Multigraph.ncard_touching_le {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {d : ℕ} (hd : G.MaxDegreeLE d) (S : Finset V) : (G.touching ↑S).ncard ≤ d * S.card

The incident-edge union pays once per edge, at most the degree budget per vertex.

theorem Complexity.Frontier.Multigraph.card_edges_le {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Fintype V] {d : ℕ} (hd : G.MaxDegreeLE d) : Nat.card E ≤ d * Fintype.card V

theorem Complexity.Frontier.Multigraph.sum_degree_mul {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Fintype V] [Fintype E] (hl : G.Loopless) (w : V → ℕ) : ∑ v : V, (G.edgesAt v).ncard * w v = ∑ e : E, (w (G.src e) + w (G.tgt e))

Weighted handshaking, counting parallel edges with multiplicity.

theorem Complexity.Frontier.Multigraph.core_density {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Fintype V] [Fintype E] (hl : G.Loopless) {d : ℕ} (hlo : ∀ (v : V), 3 ≤ (G.edgesAt v).ncard) (hhi : G.MaxDegreeLE d) (hadj : ∀ (e : E), d + 3 ≤ (G.edgesAt (G.src e)).ncard + (G.edgesAt (G.tgt e)).ncard) : 3 * d * Fintype.card V ≤ (d + 3) * Fintype.card E

Terminal-core density in every degree: adjacent degree sums at least d + 3 force 3d |V| ≤ (d + 3) |E|.