-\theorem A~spanning tree~$T$ of a graph~$G$ is minimal iff there is no $T$-light edge in~$G$.
-
-To prove this theorem, we will use a notion of edge exchanges, similar to Steinitz theorem
-in linear algebra or the exchanges in matroid theory.
-\FIXME{reference}
-
-\defn For a tree~$T$ and edges $e\in T$ and $f\not\in T$, the \df{exchange}
-XXXXXX
-
-For the other implication, we will make use of the following lemmata, again
-based on exchange of edges:
-
-{\narrower
-\lemman{Exchange property of spanning trees}
-Let $T$ and $T'$ be spanning trees of a common graph~$G$. Then there exists
-a sequence
-
-}
-
-Back to the proof of the theorem:
-
-The implication $\Rightarrow$ is straightforward: If there is a $T$-light edge~$e$, there
-exists an edge $f\in T[e]$ such that $w(f)>w(e)$. Now $T-f$ is a forest of two trees
-with endpoints of~$e$ located in different components, so adding $e$ to this forest
-must restore connectivity and $T'=T-f+e$ is another spanning tree with weight $w(T') = w(T)-w(f)+w(e) < w(T)$.
-Hence $T$ could not have been minimal.
-
-
-%\:For a disconnected graph~$G$, we define the \df{(minimal) spanning forest (or MSF)}
-% as an union of (minimal) spanning trees of its connected components.
+\rem
+Please note that the above properties also apply to tree edges
+which by definition cover only themselves and therefore they are always heavy.
+
+\lemma\thmid{lightlemma}%
+Let $T$ be a spanning tree. If there exists a $T$-light edge, then~$T$
+is not minimal.
+
+\proof
+If there is a $T$-light edge~$e$, then there exists an edge $f\in T[e]$ such
+that $w(f)>w(e)$. Now $T-f$ is a forest of two trees with endpoints of~$e$
+located in different components, so adding $e$ to this forest must restore
+connectivity and $T':=T-f+e$ is another spanning tree with weight $w(T')
+= w(T)-w(f)+w(e) < w(T)$. Hence $T$ could not have been minimal.
+\qed
+
+The converse of this lemma is also true and to prove it, we will once again use
+technique of transforming trees by \df{exchanges} of edges. In the proof of the
+lemma, we have made use of the fact that whenever we exchange an edge~$e$ of
+a spanning tree for another edge~$f$ covered by~$e$, the result is again
+a spanning tree. In fact, it is possible to transform any spanning tree
+to any other spanning tree by a sequence of exchanges.
+
+\lemman{Exchange property for trees}
+Let $T$ and $T'$ be spanning trees of a common graph. Then there exists
+a sequence of edge exchanges which transforms $T$ to~$T'$. More formally,
+there exists a sequence of spanning trees $T=T_0,T_1,\ldots,T_k=T'$ such that
+$T_{i+1}=T_i - e_i + e_i^\prime$ where $e_i\in T_i$ and $e_i^\prime\in T'$.
+
+\proof
+By induction on $d(T,T'):=\vert T\symdiff T'\vert$. When $d(T,T')=0$, then
+both trees are identical and an empty sequence suffices. Otherwise, the trees are different,
+but they are of the same size, so there must exist an edge $e'\in T'\setminus T$.
+The cycle $T[e']+e'$ cannot be wholly contained in~$T'$, so there also must
+exist an edge $e\in T[e']\setminus T'$. Exchanging $e$ for~$e'$ yields a spanning
+tree $T^*:=T-e+e'$ such that $d(T^*,T')=d(T,T')-2$ and we can apply the induction
+hypothesis to $T^*$ and $T'$ to get the rest of the exchange sequence.
+\qed
+
+\lemman{Monotone exchanges}
+\thmid{monoex}
+Let $T$ be a spanning tree such that there are no $T$-light edges and $T$
+be an arbitrary spanning tree. Then there exists a sequence of edge exchanges
+transforming $T$ to~$T'$ such that the weight does not increase in any step.
+
+\proof
+We improve the argument from the previous proof, refining the induction step.
+When we exchange $e\in T$ for $e'\in T'\setminus T$ such that $e\in T[e']$,
+the weight never drops, since $e'$ is not a $T$-light edge and therefore
+$w(e') \ge w(e)$, so $w(T^*)=w(T)-w(e)+w(e')\le w(T)$.
+
+To allow the induction to proceed, we have to make sure that there are still
+no light edges with respect to~$T^*$. In fact, it is enough to avoid $T^*$-light
+edges in $T'\setminus T^*$, since these are the only edges considered by the
+induction step. Instead of picking $e'$ arbitrarily, we will pick the lightest
+edge available. Now consider an edge $f\in T'\setminus T^*$. We want to show
+that $f$ is heavier than all edges on $T^*[f]$.
+
+The path $T^*[f]$ is either the original path $T[f]$ (if $e\not\in T[f]$)
+or $T[f] \symdiff C$, where $C$ is the cycle $T[e']+e$. The first case is
+trivial, in the second case $w(f)\ge w(e')$ and all other edges on~$C$
+are lighter than~$e'$.
+\qed
+
+\theorem
+A~spanning tree~$T$ is minimal iff there is no $T$-light edge.
+
+\proof
+If~$T$ is minimal, then by Lemma~\thmref{lightlemma} there are no $T$-light
+edges.
+Conversely, when $T$ is a spanning tree without $T$-light edges
+and $T_{min}$ is an arbitrary minimal spanning tree, then according to the Monotone
+exchange lemma~\thmref{monoex} there exists a non-decreasing sequence
+of exchanges transforming $T$ to $T_{min}$, so $w(T)\le w(T_{min})$
+and thus $T$~is also minimal.
+\qed
projects / saga.git / commitdiff