Lax17.WellLinkednessBoosting
Well-linkedness boosting
concepts/Lax17/WellLinkednessBoosting.lean · lax-17
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Evidence
Each proof establishes this claim relative to its assumptions.
Theorem
In bounded degree, edge well-linkedness can be boosted to node well-linkedness after losing only a constant-factor number of terminals.
Lean source view on GitHub
| 1 | import Lax17.Degree |
| 2 | import Lax17.Linkedness |
| 3 | import Lax17.PathOfSets |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Well-linkedness boosting |
| 8 | type: theorem |
| 9 | --- |
| 10 | In bounded degree, edge well-linkedness can be boosted to node |
| 11 | well-linkedness after losing only a constant-factor number of terminals. |
| 12 | -/ |
| 13 | |
| 14 | namespace Lax17.WellLinkednessBoosting |
| 15 | |
| 16 | universe u |
| 17 | |
| 18 | /-- In a connected cluster of a graph of maximum degree `Δ ≥ 3`, an |
| 19 | edge-well-linked terminal set of size `κ` contains a node-well-linked subset |
| 20 | of size at least `⌊κ / (4Δ)⌋`. -/ |
| 21 | axiom wellLinkednessBoosting : |
| 22 | ∀ {V : Type u} [Fintype V] [DecidableEq V] |
| 23 | (G : SimpleGraph V) (C T : Finset V) (Δ κ : ℕ), |
| 24 | Lax17.PathOfSets.IsCluster G C → |
| 25 | Lax17.Degree.MaximumAtMost G Δ → |
| 26 | 3 ≤ Δ → |
| 27 | T.card = κ → |
| 28 | Lax17.Linkedness.EdgeWellLinkedIn G C T → |
| 29 | ∃ T' : Finset V, |
| 30 | T' ⊆ T ∧ κ / (4 * Δ) ≤ T'.card ∧ |
| 31 | Lax17.Linkedness.NodeWellLinkedIn G C T' |
| 32 | |
| 33 | end Lax17.WellLinkednessBoosting |
| 34 |
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