Lax Lean Archive

Linked terminal sets

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

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Two terminal sets are linked inside a cluster when equally large subsets can be joined by that many vertex-disjoint paths contained in the cluster. A terminal set is node-well-linked when every two disjoint equally large subsets of it are linked. The edge versions replace vertex-disjointness by edge-disjointness.

    Concept map
    2 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lax17.Paths
    2
    3/-!
    4---
    5title: Linked terminal sets
    6type: definition
    7---
    8Two terminal sets are linked inside a cluster when equally large subsets can
    9be joined by that many vertex-disjoint paths contained in the cluster. A
    10terminal set is node-well-linked when every two disjoint equally large subsets
    11of it are linked. The edge versions replace vertex-disjointness by
    12edge-disjointness.
    13-/
    14
    15namespace Lax17.Linkedness
    16
    17universe u
    18
    19open Lax17.Paths
    20
    21/-- `A` and `B` are node-linked by the maximum possible number of
    22vertex-disjoint paths contained in `C`. -/
    23def NodeLinkedIn {V : Type u} [DecidableEq V]
    24 (G : SimpleGraph V) (C A B : Finset V) : Prop :=
    25 A ⊆ C ∧ B ⊆ C ∧ Disjoint A B ∧
    26 ∀ ⦃A' B' : Finset V⦄, A' ⊆ A → B' ⊆ B →
    27 ∃ P : VertexLinkage G A' B' (min A'.card B'.card),
    28 ∀ i : Fin (min A'.card B'.card), (P.path i).StaysIn C
    29
    30/-- `X` is node-well-linked inside `C`. -/
    31def NodeWellLinkedIn {V : Type u} [DecidableEq V]
    32 (G : SimpleGraph V) (C X : Finset V) : Prop :=
    33 X ⊆ C ∧
    34 ∀ ⦃A B : Finset V⦄, A ⊆ X → B ⊆ X → Disjoint A B →
    35 ∃ P : VertexLinkage G A B (min A.card B.card),
    36 ∀ i : Fin (min A.card B.card), (P.path i).StaysIn C
    37
    38/-- `A` and `B` are edge-linked by the maximum possible number of
    39edge-disjoint paths contained in `C`. -/
    40def EdgeLinkedIn {V : Type u} [DecidableEq V]
    41 (G : SimpleGraph V) (C A B : Finset V) : Prop :=
    42 A ⊆ C ∧ B ⊆ C ∧ Disjoint A B ∧
    43 ∀ ⦃A' B' : Finset V⦄, A' ⊆ A → B' ⊆ B →
    44 ∃ P : EdgeLinkage G A' B' (min A'.card B'.card),
    45 ∀ i : Fin (min A'.card B'.card), (P.path i).StaysIn C
    46
    47/-- `X` is edge-well-linked inside `C`. -/
    48def EdgeWellLinkedIn {V : Type u} [DecidableEq V]
    49 (G : SimpleGraph V) (C X : Finset V) : Prop :=
    50 X ⊆ C ∧
    51 ∀ ⦃A B : Finset V⦄, A ⊆ X → B ⊆ X → Disjoint A B →
    52 ∃ P : EdgeLinkage G A B (min A.card B.card),
    53 ∀ i : Fin (min A.card B.card), (P.path i).StaysIn C
    54
    55/-- Cut-based edge well-linkedness with parameter `numerator / denominator`.
    56Every partition of the whole vertex set cuts the corresponding fraction of
    57the smaller terminal side. -/
    58def ScaledEdgeWellLinked {V : Type u} [Fintype V] [DecidableEq V]
    59 (G : SimpleGraph V) (T : Finset V)
    60 (numerator denominator : ℕ) : Prop :=
    61 0 < numerator ∧ numerator ≤ denominator ∧
    62 ∀ X Y : Finset V,
    63 X ∪ Y = Finset.univ → Disjoint X Y →
    64 numerator * min (X ∩ T).card (Y ∩ T).card ≤
    65 denominator * (edgeBoundary G X Y).card
    66
    67end Lax17.Linkedness
    68
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…