Counting the edges of multigraphs

Parallel edges are distinct elements of the edge type throughout. The underlying simple graph (Cslib.Circuits.Frontier.Multigraph.toSimpleGraph), with loops and multiplicities discarded, is the graph in which the Gaussian layouts measure distances, and its degrees are at most those of the multigraph (Cslib.Circuits.Frontier.Multigraph.MaxDegreeLE.degree_toSimpleGraph_le). The multigraph itself supplies degrees, cuts, and the density of cores.

Core density (Cslib.Circuits.Frontier.Multigraph.core_density). Let a loopless multigraph of maximum degree d have every vertex of degree at least three, and the ends of every edge of degrees summing to at least d + 3. Give each vertex the weight d + 3 - deg v. The weights at the ends of an edge sum to at most d + 3, and a vertex of degree j + 3 ≤ d has deg v · weight v = (j + 3)(d - j) ≥ 3 d. So the weighted handshake lemma (Cslib.Circuits.Frontier.Multigraph.sum_ncard_incidenceSet_mul) gives 3 d |V| ≤ (d + 3) |E|.

Main results

• Cslib.Circuits.Frontier.Multigraph.MaxDegreeLE.degree_toSimpleGraph_le: the underlying simple graph has no larger degrees.
• Cslib.Circuits.Frontier.Multigraph.ncard_touching_le: at most d |S| edges touch S.
• Cslib.Circuits.Frontier.Multigraph.card_le_mul_card: at most d |V| edges.
• Cslib.Circuits.Frontier.Multigraph.sum_ncard_incidenceSet_mul: the weighted handshake lemma.
• Cslib.Circuits.Frontier.Multigraph.core_density: the density of cores.

theorem Cslib.Circuits.Frontier.Multigraph.MaxDegreeLE.degree_toSimpleGraph_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Fintype V] [DecidableRel G.toSimpleGraph.Adj] [Finite E] {d : ℕ} (h : G.MaxDegreeLE d) (v : V) : G.toSimpleGraph.degree v ≤ d

The underlying simple graph has no larger degrees. Every neighbour of v in the underlying simple graph is the other end of an edge at v.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_touching_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite E] [Finite V] {d : ℕ} (hd : G.MaxDegreeLE d) (S : Set V) : (G.touching S).ncard ≤ d * S.ncard

In maximum degree d, at most d |S| edges touch a set of vertices S.

theorem Cslib.Circuits.Frontier.Multigraph.card_le_mul_card {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite E] [Finite V] {d : ℕ} (hd : G.MaxDegreeLE d) : Nat.card E ≤ d * Nat.card V

In maximum degree d, a multigraph has at most d |V| edges.

theorem Cslib.Circuits.Frontier.Multigraph.sum_ncard_incidenceSet_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.incidenceSet v).ncard * w v = ∑ e : E, (w (G.src e) + w (G.tgt e))

The weighted handshake lemma. In a finite loopless multigraph, the numbers of edges at the vertices, weighted by w, add up to the sum over the edges of the weights of their ends.

theorem Cslib.Circuits.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.incidenceSet v).ncard) (hhi : G.MaxDegreeLE d) (hadj : ∀ (e : E), d + 3 ≤ (G.incidenceSet (G.src e)).ncard + (G.incidenceSet (G.tgt e)).ncard) : 3 * d * Fintype.card V ≤ (d + 3) * Fintype.card E

The density of cores. In a loopless multigraph of maximum degree d in which every vertex has at least three edges and the ends of every edge have at least d + 3 edges between them, counted with multiplicity, 3 d |V| ≤ (d + 3) |E|.