Few edges in the graph induced by short routes

Lax263307.InducedRouteEdges · concepts/Lax263307/InducedRouteEdges.lean · lax-263307

proven

Loading review…

Natural Language Statement

Theorem

Suppose an induced almost-embedding of a graph $H$ of maximum degree at most $d$ uses at most $L$ host vertices per route. The union of its routes has at most $|E(H)|L$ vertices. Its induced graph has maximum degree at most $2dL$ , and therefore at most $d|E(H)|L^2$ edges.

Concept map

5 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax263307.InducedRouteEdges

⊢Lax263307Proofs.InducedRouteEdges.edge_bound

Lean source view on GitHub

Show types on hover

1	import Lax263307.AlmostEmbeddings
2	import Mathlib.Combinatorics.SimpleGraph.DegreeSum
3
4	/-!
5	---
6	title: Few edges in the graph induced by short routes
7	type: theorem
8	---
9	Suppose an induced almost-embedding of a graph $H$ of maximum degree at most
10	$d$ uses at most $L$ host vertices per route. The union of its routes has
11	at most $\|E(H)\|L$ vertices. Its induced graph has maximum degree at most
12	$2dL$ , and therefore at most $d\|E(H)\|L^2$ edges.
13
14	# Attribution
15
16	The induced edge-count estimate for retained short paths in Bonnet–Chang,
17	proof of Lemma 11.
18	-/
19
20	namespace Lax263307.InducedRouteEdges
21
22	open AlmostEmbeddings
23
24	/-- All host vertices used by some edge route. -/
25	noncomputable def routeUnion {t n : ℕ} {H : SimpleGraph (Fin t)}
26	[DecidableRel H.Adj] {G : SimpleGraph (Fin n)} (E : AlmostEmbedding H G) : Finset (Fin n) := by
27	classical
28	exact Finset.univ.biUnion E.route
29
30	/-- Bounded-length induced routes induce few host edges. -/
31	axiom edge_bound {t n : ℕ} (H : SimpleGraph (Fin t)) [DecidableRel H.Adj]
32	(G : SimpleGraph (Fin n)) (E : AlmostEmbedding H G) (d L : ℕ)
33	(induced : IsInduced E) (degree_bound : ∀ v, H.degree v ≤ d)
34	(length_bound : ∀ e, (E.route e).card ≤ L) :
35	(G.induce (↑(routeUnion E) : Set (Fin n))).edgeSet.ncard ≤
36	d * H.edgeSet.ncard * L ^ 2
37
38	end Lax263307.InducedRouteEdges
39