No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
Let be a set system on a finite ground set and let T be a spanning tree of that ground set. A member X of crosses an edge of T when exactly one endpoint of the edge belongs to X. Its tree crossing count is the number of crossed edges, and the crossing number of T is the largest such count over all members of . A Welzl tree of crossing number at most k is a spanning tree whose crossing number is at most k.
Lean source view on GitHub
| 1 | import Lax195003.WelzlOrders |
| 2 | import Mathlib.Combinatorics.SimpleGraph.Acyclic |
| 3 | import Mathlib.Data.Nat.Lattice |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Welzl trees |
| 8 | type: definition |
| 9 | --- |
| 10 | Let `𝒜` be a set system on a finite ground set and let *T* be a spanning |
| 11 | tree of that ground set. A member *X* of `𝒜` crosses an edge of *T* when |
| 12 | exactly one endpoint of the edge belongs to *X*. Its tree crossing count is |
| 13 | the number of crossed edges, and the crossing number of *T* is the largest |
| 14 | such count over all members of `𝒜`. A Welzl tree of crossing number at |
| 15 | most *k* is a spanning tree whose crossing number is at most *k*. |
| 16 | |
| 17 | # Formalization notes |
| 18 | |
| 19 | An edge is represented by its unordered pair of endpoints. The cut of *X* |
| 20 | is defined with `Sym2.fromRel` from the symmetric relation saying that the |
| 21 | endpoints lie on opposite sides of *X*; intersecting this cut with the edge |
| 22 | set of *T* therefore counts every crossed edge exactly once. |
| 23 | |
| 24 | A spanning tree is a `SimpleGraph.IsTree` on the entire ground type, so no |
| 25 | separate spanning field is needed. The crossing number is a natural |
| 26 | supremum, following the Welzl-order definition. It is bounded by the finite |
| 27 | number of pairs of ground elements, and `sSup ∅ = 0` supplies the expected |
| 28 | value for an empty set system. `IsWelzlTree` is a proposition rather than a |
| 29 | structure carrying data already determined by the tree and set system. |
| 30 | -/ |
| 31 | |
| 32 | namespace Lax485480.WelzlTrees |
| 33 | |
| 34 | open Lax195003.WelzlOrders |
| 35 | |
| 36 | /-- The symmetric cut relation determined by `X`: its two arguments lie on |
| 37 | opposite sides of `X`. -/ |
| 38 | def SeparatedBy {V : Type*} (X : Set V) (u v : V) : Prop := |
| 39 | u ∈ X ↔ v ∉ X |
| 40 | |
| 41 | /-- The unordered pairs whose endpoints lie on opposite sides of `X`. -/ |
| 42 | def cutEdges {V : Type*} (X : Set V) : Set (Sym2 V) := |
| 43 | Sym2.fromRel (r := SeparatedBy X) (by |
| 44 | intro u v |
| 45 | simp only [SeparatedBy] |
| 46 | tauto) |
| 47 | |
| 48 | /-- The number of edges of `T` crossed by `X`. -/ |
| 49 | noncomputable def treeCrossingCount {n : ℕ} (T : SimpleGraph (Fin n)) |
| 50 | (X : Set (Fin n)) : ℕ := |
| 51 | (T.edgeSet ∩ cutEdges X).ncard |
| 52 | |
| 53 | /-- The largest tree crossing count of a member of `𝒜`. -/ |
| 54 | noncomputable def treeCrossingNumber {n : ℕ} (𝓕 : SetSystem (Fin n)) |
| 55 | (T : SimpleGraph (Fin n)) : ℕ := |
| 56 | sSup {k : ℕ | ∃ X ∈ 𝓕, k = treeCrossingCount T X} |
| 57 | |
| 58 | /-- `T` is a spanning Welzl tree of crossing number at most `k` for `𝒜`. -/ |
| 59 | def IsWelzlTree {n : ℕ} (𝓕 : SetSystem (Fin n)) |
| 60 | (T : SimpleGraph (Fin n)) (k : ℕ) : Prop := |
| 61 | T.IsTree ∧ treeCrossingNumber 𝓕 T ≤ k |
| 62 | |
| 63 | end Lax485480.WelzlTrees |
| 64 |
Formalization notes
An edge is represented by its unordered pair of endpoints. The cut of X is defined with from the symmetric relation saying that the endpoints lie on opposite sides of X; intersecting this cut with the edge set of T therefore counts every crossed edge exactly once.
A spanning tree is a on the entire ground type, so no separate spanning field is needed. The crossing number is a natural supremum, following the Welzl-order definition. It is bounded by the finite number of pairs of ground elements, and supplies the expected value for an empty set system. is a proposition rather than a structure carrying data already determined by the tree and set system.
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments