Bounded-degree spanning-tree relaxation

Lax17.SpanningTreeRounding · concepts/Lax17/SpanningTreeRounding.lean · lax-17

definition

Loading review…

Natural Language Statement

Definition

A feasible bounded-degree spanning-tree point assigns nonnegative rational weights to the edges, has total weight $|V|-1$ , satisfies every forest inequality, and has fractional degree at most $B$ at every vertex. This is the unweighted relaxation used by the Singh–Lau rounding theorem.

Concept map

2 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Data.Rat.Defs
2	import Lax17.Degree
3
4	/-!
5	---
6	title: Bounded-degree spanning-tree relaxation
7	type: definition
8	---
9	A feasible bounded-degree spanning-tree point assigns nonnegative rational
10	weights to the edges, has total weight $\|V\|-1$, satisfies every forest
11	inequality, and has fractional degree at most $B$ at every vertex. This is
12	the unweighted relaxation used by the Singh--Lau rounding theorem.
13	-/
14
15	namespace Lax17.SpanningTreeRounding
16
17	universe u
18
19	open Finset
20
21	/-- Both endpoints of an unordered pair lie in `S`. -/
22	def PairInside {V : Type u} [DecidableEq V]
23	(S : Finset V) (e : Sym2 V) : Prop :=
24	e.toFinset ⊆ S
25
26	/-- The finite edge set of `G`. -/
27	noncomputable def edges {V : Type u} [Fintype V]
28	(G : SimpleGraph V) : Finset (Sym2 V) :=
29	G.edgeSet.toFinite.toFinset
30
31	/-- The edges of `G` with both endpoints in `S`. -/
32	noncomputable def internalEdges {V : Type u} [Fintype V] [DecidableEq V]
33	(G : SimpleGraph V) (S : Finset V) : Finset (Sym2 V) :=
34	@Finset.filter (Sym2 V) (PairInside S) (Classical.decPred _) (edges G)
35
36	/-- The edges of `G` incident with `v`. -/
37	noncomputable def incidentEdges {V : Type u} [Fintype V] [DecidableEq V]
38	(G : SimpleGraph V) (v : V) : Finset (Sym2 V) :=
39	(edges G).filter fun e => v ∈ e
40
41	/-- A feasible point of the bounded-degree spanning-tree relaxation. -/
42	structure FeasiblePoint {V : Type u} [Fintype V] [DecidableEq V]
43	(G : SimpleGraph V) (B : ℕ) where
44	weight : Sym2 V → ℚ
45	nonnegative : ∀ e : Sym2 V, e ∈ edges G → 0 ≤ weight e
46	total :
47	(edges G).sum weight = (Fintype.card V - 1 : ℕ)
48	forest :
49	∀ S : Finset V, S ≠ Finset.univ →
50	(internalEdges G S).sum weight ≤ (S.card - 1 : ℕ)
51	degree :
52	∀ v : V, (incidentEdges G v).sum weight ≤ B
53
54	end Lax17.SpanningTreeRounding
55