SimpleGraph Bridge for Kruskal's Algorithm

This module connects the multigraph and DisjointSet.Partition formulation of Kruskal's algorithm in CslibFrontier.Algorithms.Lean.Kruskal.Basic to Mathlib's SimpleGraph, SimpleGraph.IsAcyclic, maximal acyclic subgraphs (Maximal (fun H => H ≤ G ∧ H.IsAcyclic)), and SimpleGraph.IsTree.

Main definitions

• WeightedEdge.sym2: unordered vertex pair s(e.u, e.v) : Sym2 (Fin n) of a weighted edge.
• toSimpleGraph: simple graph on Fin n spanned by an edge list (discarding self-loops and collapsing parallel edges).
• graphEdges: canonical computable enumeration (u < v with G.Adj u v) of the undirected edges of G : SimpleGraph (Fin n) weighted by w : Sym2 (Fin n) → W.
• kruskalGraph, kruskalGraphM: pure and TimeM Cost Kruskal runners directly on a weighted SimpleGraph (Fin n).

Main results

• rel_edgePartition_iff_reachable, numComponents_edgePartition_eq_one_iff_connected: equivalence between edgePartition connectivity and SimpleGraph.Reachable / SimpleGraph.Connected.
• isAcyclic_iff_toSimpleGraph: exact characterization IsAcyclic F ↔ (toSimpleGraph F).IsAcyclic ∧ (F.map WeightedEdge.sym2).Nodup ∧ ∀ e ∈ F, e.u ≠ e.v.
• toSimpleGraph_kruskalEdges_maximal_isAcyclic, toSimpleGraph_kruskalEdges_isTree: the simple graph spanned by kruskalEdges es is a maximal acyclic subgraph of toSimpleGraph es (and a SimpleGraph.IsTree with n - 1 edges when toSimpleGraph es is connected).
• kruskalGraph_maximal_isAcyclic, sum_edgeFinset_kruskalGraph_le_of_maximal_isAcyclic: toSimpleGraph (kruskalGraph G w) is a minimum-weight Mathlib spanning forest of G.
• kruskalGraph_isTree, sum_edgeFinset_kruskalGraph_le_of_isTree: when G.Connected, toSimpleGraph (kruskalGraph G w) is a minimum-weight Mathlib spanning tree of G.
• eq_toSimpleGraph_kruskalGraph_of_injOn, eq_toSimpleGraph_kruskalGraph_of_isTree_of_injOn: when w is injective on G.edgeSet (generalizing Kruskal, Opening paragraph, Construction A, and uniqueness proof, pp. 48–50 to disconnected simple graphs and ordered cancellative monoids), the minimum spanning forest (and minimum spanning tree when connected) is unique as a SimpleGraph (Fin n).
• kruskalGraphM_comparisons_le, kruskalGraphM_ufSteps_le, kruskalGraphM_total_le: explicit sorting comparison and disjoint-set step bounds in terms of m = G.edgeFinset.card and n.

Cost model and limitations

kruskalGraphM G w := kruskalM (graphEdges G w) charges only the List.mergeSortM weight comparisons (Cost.comparisons) and post-initialization DisjointSet.UnionFind forest steps (Cost.ufSteps) performed on the extracted m-edge list. The pure graphEdges G w enumeration pass (which inspects all n² ordered pairs in List.finRange n, evaluating decide (G.Adj u v) and w s(u, v) on matching edges) and DisjointSet.UnionFind.init n (O(n) initialization) carry 0 TimeM Cost charge; callers that already hold an explicit edge list should invoke kruskalM directly.

References

• J. B. Kruskal, Jr., On the Shortest Spanning Subtree of a Graph and the Traveling Salesman Problem
• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Chapter 23

Edge-list projection to SimpleGraph (Fin n)

def Cslib.Algorithms.Lean.Kruskal.WeightedEdge.sym2 {n : ℕ} {W : Type} (e : WeightedEdge n W) : Sym2 (Fin n)

Unordered endpoint pair s(e.u, e.v) of a weighted edge.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.WeightedEdge.sym2_eq {n : ℕ} {W : Type} (e : WeightedEdge n W) : e.sym2 = s(e.u, e.v)

def Cslib.Algorithms.Lean.Kruskal.toSimpleGraph {n : ℕ} {W : Type} (es : List (WeightedEdge n W)) : SimpleGraph (Fin n)

Simple graph on Fin n spanned by es (discarding self-loops and collapsing parallel edges).

@[instance_reducible]

instance Cslib.Algorithms.Lean.Kruskal.instDecidableRelToSimpleGraphAdj {n : ℕ} {W : Type} (es : List (WeightedEdge n W)) : DecidableRel (toSimpleGraph es).Adj

theorem Cslib.Algorithms.Lean.Kruskal.toSimpleGraph_adj {n : ℕ} {W : Type} (es : List (WeightedEdge n W)) (x y : Fin n) : (toSimpleGraph es).Adj x y ↔ s(x, y) ∈ List.map WeightedEdge.sym2 es ∧ x ≠ y

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.toSimpleGraph_nil {n : ℕ} {W : Type} : toSimpleGraph [] = ⊥

theorem Cslib.Algorithms.Lean.Kruskal.toSimpleGraph_cons {n : ℕ} {W : Type} (e : WeightedEdge n W) (es : List (WeightedEdge n W)) : toSimpleGraph (e :: es) = SimpleGraph.edge e.u e.v ⊔ toSimpleGraph es

theorem Cslib.Algorithms.Lean.Kruskal.toSimpleGraph_append {n : ℕ} {W : Type} (es₁ es₂ : List (WeightedEdge n W)) : toSimpleGraph (es₁ ++ es₂) = toSimpleGraph es₁ ⊔ toSimpleGraph es₂

theorem Cslib.Algorithms.Lean.Kruskal.toSimpleGraph_singleton {n : ℕ} {W : Type} (e : WeightedEdge n W) : toSimpleGraph [e] = SimpleGraph.edge e.u e.v

theorem Cslib.Algorithms.Lean.Kruskal.Perm.toSimpleGraph_eq {n : ℕ} {W : Type} {es₁ es₂ : List (WeightedEdge n W)} (h : es₁.Perm es₂) : toSimpleGraph es₁ = toSimpleGraph es₂

Permuting an edge list preserves toSimpleGraph.

theorem Cslib.Algorithms.Lean.Kruskal.Subperm.toSimpleGraph_le {n : ℕ} {W : Type} {es₁ es₂ : List (WeightedEdge n W)} (h : es₁.Subperm es₂) : toSimpleGraph es₁ ≤ toSimpleGraph es₂

A sub-multiset (Subperm) spans a subgraph.

Reachability, connectedness, and acyclicity correspondence

theorem Cslib.Algorithms.Lean.Kruskal.rel_edgePartition_iff_reachable {n : ℕ} {W : Type} (es : List (WeightedEdge n W)) (x y : Fin n) : (edgePartition es).rel x y = true ↔ (toSimpleGraph es).Reachable x y

Exact correspondence between partition equivalence in edgePartition es and walk reachability in toSimpleGraph es.

theorem Cslib.Algorithms.Lean.Kruskal.edgePartition_eq_iff_reachable_eq {n : ℕ} {W₁ W₂ : Type} (es₁ : List (WeightedEdge n W₁)) (es₂ : List (WeightedEdge n W₂)) : edgePartition es₁ = edgePartition es₂ ↔ (toSimpleGraph es₁).Reachable = (toSimpleGraph es₂).Reachable

Two edge lists induce the same edgePartition iff their simple graphs have the same Reachable relation.

theorem Cslib.Algorithms.Lean.Kruskal.numComponents_edgePartition_eq_one_iff_connected {n : ℕ} {W : Type} (es : List (WeightedEdge n W)) : (edgePartition es).numComponents = 1 ↔ (toSimpleGraph es).Connected

edgePartition es has a single connected component iff toSimpleGraph es is Connected (including the empty-graph boundary n = 0, where both sides are false).

theorem Cslib.Algorithms.Lean.Kruskal.isAcyclic_iff_toSimpleGraph {n : ℕ} {W : Type} (F : List (WeightedEdge n W)) : IsAcyclic F ↔ (toSimpleGraph F).IsAcyclic ∧ (List.map WeightedEdge.sym2 F).Nodup ∧ ∀ e ∈ F, e.u ≠ e.v

Exact equivalence between edge-list acyclicity IsAcyclic F and simple-graph acyclicity (toSimpleGraph F).IsAcyclic without parallel edges or self-loops.

theorem Cslib.Algorithms.Lean.Kruskal.IsAcyclic.toSimpleGraph_isAcyclic {n : ℕ} {W : Type} {F : List (WeightedEdge n W)} (hF : IsAcyclic F) : (toSimpleGraph F).IsAcyclic

theorem Cslib.Algorithms.Lean.Kruskal.IsAcyclic.nodup_map_sym2 {n : ℕ} {W : Type} {F : List (WeightedEdge n W)} (hF : IsAcyclic F) : (List.map WeightedEdge.sym2 F).Nodup

theorem Cslib.Algorithms.Lean.Kruskal.edgeFinset_toSimpleGraph_of_no_loops {n : ℕ} {W : Type} {es : List (WeightedEdge n W)} (hloop : ∀ e ∈ es, e.u ≠ e.v) : (toSimpleGraph es).edgeFinset = (List.map WeightedEdge.sym2 es).toFinset

When es has no self-loops, (toSimpleGraph es).edgeFinset is (es.map sym2).toFinset.

theorem Cslib.Algorithms.Lean.Kruskal.IsAcyclic.card_edgeFinset_toSimpleGraph {n : ℕ} {W : Type} {F : List (WeightedEdge n W)} (hF : IsAcyclic F) : (toSimpleGraph F).edgeFinset.card = F.length

An acyclic edge list F has (toSimpleGraph F).edgeFinset.card = F.length.

theorem Cslib.Algorithms.Lean.Kruskal.IsAcyclic.sum_edgeFinset_toSimpleGraph {n : ℕ} {W : Type} [AddCommMonoid W] {F : List (WeightedEdge n W)} (hF : IsAcyclic F) (w : Sym2 (Fin n) → W) (hw : ∀ e ∈ F, e.weight = w e.sym2) : ∑ z ∈ (toSimpleGraph F).edgeFinset, w z = totalWeight F

When F is acyclic and every edge in F carries weight w e.sym2, totalWeight F equals ∑ z ∈ (toSimpleGraph F).edgeFinset, w z.

theorem Cslib.Algorithms.Lean.Kruskal.IsSpanningForest.toSimpleGraph_maximal_isAcyclic {n : ℕ} {W : Type} {es F : List (WeightedEdge n W)} (hF : IsSpanningForest es F) : Maximal (fun (H : SimpleGraph (Fin n)) => H ≤ toSimpleGraph es ∧ H.IsAcyclic) (toSimpleGraph F)

Every IsSpanningForest es F projects to a Mathlib maximal acyclic subgraph of toSimpleGraph es.

theorem Cslib.Algorithms.Lean.Kruskal.toSimpleGraph_kruskalEdges_maximal_isAcyclic {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : Maximal (fun (H : SimpleGraph (Fin n)) => H ≤ toSimpleGraph es ∧ H.IsAcyclic) (toSimpleGraph (kruskalEdges es))

toSimpleGraph (kruskalEdges es) is a maximal acyclic subgraph of toSimpleGraph es.

theorem Cslib.Algorithms.Lean.Kruskal.toSimpleGraph_kruskalEdges_isTree {n : ℕ} {W : Type} [LE W] [DecidableLE W] {es : List (WeightedEdge n W)} (hconn : (toSimpleGraph es).Connected) : (toSimpleGraph (kruskalEdges es)).IsTree ∧ (kruskalEdges es).length + 1 = n

When toSimpleGraph es is connected, toSimpleGraph (kruskalEdges es) is a SimpleGraph.IsTree with (kruskalEdges es).length + 1 = n.

Canonical Kruskal runner on weighted SimpleGraph (Fin n)

def Cslib.Algorithms.Lean.Kruskal.graphEdges {n : ℕ} {W : Type} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : List (WeightedEdge n W)

Canonical computable enumeration of the undirected edges of G : SimpleGraph (Fin n): pairs (u, v) with u < v and G.Adj u v, weighted by w s(u, v). Each undirected edge in G.edgeFinset appears once.

theorem Cslib.Algorithms.Lean.Kruskal.mem_graphEdges {n : ℕ} {W : Type} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) (e : WeightedEdge n W) : e ∈ graphEdges G w ↔ e.u < e.v ∧ G.Adj e.u e.v ∧ e.weight = w s(e.u, e.v)

Exact membership predicate for graphEdges G w.

theorem Cslib.Algorithms.Lean.Kruskal.nodup_graphEdges {n : ℕ} {W : Type} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : (graphEdges G w).Nodup

(graphEdges G w) contains no duplicate edges.

theorem Cslib.Algorithms.Lean.Kruskal.nodup_map_sym2_graphEdges {n : ℕ} {W : Type} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : (List.map WeightedEdge.sym2 (graphEdges G w)).Nodup

Unordered endpoint pairs in graphEdges G w have no duplicates.

theorem Cslib.Algorithms.Lean.Kruskal.mem_map_sym2_graphEdges {n : ℕ} {W : Type} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) (x y : Fin n) : s(x, y) ∈ List.map WeightedEdge.sym2 (graphEdges G w) ↔ G.Adj x y

s(x, y) appears in (graphEdges G w).map sym2 iff G.Adj x y.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.toSimpleGraph_graphEdges {n : ℕ} {W : Type} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : toSimpleGraph (graphEdges G w) = G

toSimpleGraph (graphEdges G w) recovers G exactly.

theorem Cslib.Algorithms.Lean.Kruskal.edgeFinset_eq_toFinset_graphEdges {n : ℕ} {W : Type} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (w : Sym2 (Fin n) → W) : G.edgeFinset = (List.map WeightedEdge.sym2 (graphEdges G w)).toFinset

G.edgeFinset agrees with ((graphEdges G w).map sym2).toFinset for any Fintype G.edgeSet instance.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.length_graphEdges {n : ℕ} {W : Type} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (w : Sym2 (Fin n) → W) : (graphEdges G w).length = G.edgeFinset.card

(graphEdges G w) has length G.edgeFinset.card.

theorem Cslib.Algorithms.Lean.Kruskal.graphEdges_subperm_of_le {n : ℕ} {W : Type} {F G : SimpleGraph (Fin n)} [DecidableRel F.Adj] [DecidableRel G.Adj] (hle : F ≤ G) (w : Sym2 (Fin n) → W) : (graphEdges F w).Subperm (graphEdges G w)

If F ≤ G, graphEdges F w is a sub-multiset of graphEdges G w.

theorem Cslib.Algorithms.Lean.Kruskal.totalWeight_graphEdges {n : ℕ} {W : Type} [AddCommMonoid W] (F : SimpleGraph (Fin n)) [DecidableRel F.Adj] [Fintype ↑F.edgeSet] (w : Sym2 (Fin n) → W) : totalWeight (graphEdges F w) = ∑ z ∈ F.edgeFinset, w z

For any subgraph F, totalWeight (graphEdges F w) equals ∑ e ∈ F.edgeFinset, w e.

theorem Cslib.Algorithms.Lean.Kruskal.isSpanningForest_graphEdges_of_maximal_isAcyclic {n : ℕ} {W : Type} {F G : SimpleGraph (Fin n)} [DecidableRel F.Adj] [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) (hF : Maximal (fun (H : SimpleGraph (Fin n)) => H ≤ G ∧ H.IsAcyclic) F) : IsSpanningForest (graphEdges G w) (graphEdges F w)

Every Mathlib maximal acyclic subgraph F of G corresponds to an IsSpanningForest of graphEdges G w.

def Cslib.Algorithms.Lean.Kruskal.kruskalGraph {n : ℕ} {W : Type} [LE W] [DecidableLE W] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : List (WeightedEdge n W)

Pure Kruskal runner on a weighted SimpleGraph (Fin n).

theorem Cslib.Algorithms.Lean.Kruskal.kruskalGraph_maximal_isAcyclic {n : ℕ} {W : Type} [LE W] [DecidableLE W] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : Maximal (fun (H : SimpleGraph (Fin n)) => H ≤ G ∧ H.IsAcyclic) (toSimpleGraph (kruskalGraph G w))

toSimpleGraph (kruskalGraph G w) is a Mathlib maximal acyclic subgraph (spanning forest) of G.

theorem Cslib.Algorithms.Lean.Kruskal.sum_edgeFinset_toSimpleGraph_kruskalGraph {n : ℕ} {W : Type} [AddCommMonoid W] [LE W] [DecidableLE W] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : ∑ z ∈ (toSimpleGraph (kruskalGraph G w)).edgeFinset, w z = totalWeight (kruskalGraph G w)

The edge-finset weight sum of toSimpleGraph (kruskalGraph G w) equals totalWeight (kruskalGraph G w).

theorem Cslib.Algorithms.Lean.Kruskal.sum_edgeFinset_kruskalGraph_le_of_maximal_isAcyclic {n : ℕ} {W : Type} [AddCommMonoid W] [LinearOrder W] [IsOrderedAddMonoid W] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) (F : SimpleGraph (Fin n)) [Fintype ↑F.edgeSet] (hF : Maximal (fun (H : SimpleGraph (Fin n)) => H ≤ G ∧ H.IsAcyclic) F) : ∑ z ∈ (toSimpleGraph (kruskalGraph G w)).edgeFinset, w z ≤ ∑ z ∈ F.edgeFinset, w z

Simple-graph Kruskal spanning-forest optimality (generalizing Cormen et al., Section 23.2, MST-KRUSKAL, p. 631 from connected real-weighted graphs to arbitrary finite simple graphs over [AddCommMonoid W] [LinearOrder W] [IsOrderedAddMonoid W]): toSimpleGraph (kruskalGraph G w) minimizes ∑ e ∈ F.edgeFinset, w e over all Mathlib spanning forests F of G (without requiring DecidableRel F.Adj on competing subgraphs F).

theorem Cslib.Algorithms.Lean.Kruskal.kruskalGraph_isTree {n : ℕ} {W : Type} [LE W] [DecidableLE W] {G : SimpleGraph (Fin n)} [DecidableRel G.Adj] (hconn : G.Connected) (w : Sym2 (Fin n) → W) : (toSimpleGraph (kruskalGraph G w)).IsTree ∧ (kruskalGraph G w).length + 1 = n

When G is connected, toSimpleGraph (kruskalGraph G w) is a SimpleGraph.IsTree with n - 1 edges ((kruskalGraph G w).length + 1 = n).

theorem Cslib.Algorithms.Lean.Kruskal.sum_edgeFinset_kruskalGraph_le_of_isTree {n : ℕ} {W : Type} [AddCommMonoid W] [LinearOrder W] [IsOrderedAddMonoid W] {G : SimpleGraph (Fin n)} [DecidableRel G.Adj] (hconn : G.Connected) (w : Sym2 (Fin n) → W) (T : SimpleGraph (Fin n)) [Fintype ↑T.edgeSet] (hle : T ≤ G) (hT : T.IsTree) : ∑ z ∈ (toSimpleGraph (kruskalGraph G w)).edgeFinset, w z ≤ ∑ z ∈ T.edgeFinset, w z

Simple-graph Kruskal minimum spanning tree optimality (Cormen et al., Section 23.2, p. 631): on a connected graph G, toSimpleGraph (kruskalGraph G w) minimizes ∑ e ∈ T.edgeFinset, w e over all spanning trees T ≤ G.

theorem Cslib.Algorithms.Lean.Kruskal.eq_toSimpleGraph_kruskalGraph_of_injOn {n : ℕ} {W : Type} [AddCancelCommMonoid W] [LinearOrder W] [IsOrderedCancelAddMonoid W] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) (hinj : Set.InjOn w G.edgeSet) {F : SimpleGraph (Fin n)} [Fintype ↑F.edgeSet] (hF : Maximal (fun (H : SimpleGraph (Fin n)) => H ≤ G ∧ H.IsAcyclic) F) (hopt : ∑ z ∈ F.edgeFinset, w z ≤ ∑ z ∈ (toSimpleGraph (kruskalGraph G w)).edgeFinset, w z) : F = toSimpleGraph (kruskalGraph G w)

Distinct-weight uniqueness on simple graphs (generalizing Kruskal, Opening paragraph, Construction A, and uniqueness proof, pp. 48–50): when w is injective on G.edgeSet, any minimum-weight spanning forest F of G is equal as a SimpleGraph (Fin n) to toSimpleGraph (kruskalGraph G w).

theorem Cslib.Algorithms.Lean.Kruskal.eq_toSimpleGraph_kruskalGraph_of_isTree_of_injOn {n : ℕ} {W : Type} [AddCancelCommMonoid W] [LinearOrder W] [IsOrderedCancelAddMonoid W] {G : SimpleGraph (Fin n)} [DecidableRel G.Adj] (hconn : G.Connected) (w : Sym2 (Fin n) → W) (hinj : Set.InjOn w G.edgeSet) {T : SimpleGraph (Fin n)} [Fintype ↑T.edgeSet] (hle : T ≤ G) (hT : T.IsTree) (hopt : ∑ z ∈ T.edgeFinset, w z ≤ ∑ z ∈ (toSimpleGraph (kruskalGraph G w)).edgeFinset, w z) : T = toSimpleGraph (kruskalGraph G w)

Connected specialization of eq_toSimpleGraph_kruskalGraph_of_injOn: when G is connected and w is injective on G.edgeSet, toSimpleGraph (kruskalGraph G w) is the unique minimum-weight spanning tree of G.

TimeM Cost Kruskal runner on SimpleGraph (Fin n)

def Cslib.Algorithms.Lean.Kruskal.kruskalGraphM {n : ℕ} {W : Type} [LE W] [DecidableLE W] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : TimeM Cost (Output n W)

Execute Kruskal's algorithm in TimeM Cost on the canonical edge list graphEdges G w. Note that Cost charges sorting comparisons and post-initialization UnionFind forest steps on the extracted m-edge list; the pure graphEdges G w enumeration (Θ(n²) adjacency/weight checks) and DisjointSet.UnionFind.init n carry 0 TimeM Cost charge.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.kruskalGraphM_forest {n : ℕ} {W : Type} [LE W] [DecidableLE W] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : (kruskalGraphM G w).ret.forest = kruskalGraph G w

theorem Cslib.Algorithms.Lean.Kruskal.kruskalGraphM_comparisons_le {n : ℕ} {W : Type} [LE W] [DecidableLE W] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : (kruskalGraphM G w).time.comparisons ≤ G.edgeFinset.card * Nat.clog 2 G.edgeFinset.card

Sorting comparison bound for kruskalGraphM in terms of m = G.edgeFinset.card: at most m * ⌈log₂ m⌉ weight comparisons.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalGraphM_ufSteps_le {n : ℕ} {W : Type} [LE W] [DecidableLE W] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : (kruskalGraphM G w).time.ufSteps ≤ G.edgeFinset.card * (2 * Nat.log 2 n + 3)

Disjoint-set forest step bound for kruskalGraphM in terms of m = G.edgeFinset.card and n: at most m * (2 * ⌊log₂ n⌋ + 3) union-find steps.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalGraphM_total_le {n : ℕ} {W : Type} [LE W] [DecidableLE W] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (w : Sym2 (Fin n) → W) : (kruskalGraphM G w).time.total ≤ G.edgeFinset.card * Nat.clog 2 G.edgeFinset.card + G.edgeFinset.card * (2 * Nat.log 2 n + 3)

Combined bound on (kruskalGraphM G w).time.total in terms of m = G.edgeFinset.card and n.