Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax17.Linkedness

Linked terminal sets

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    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.

    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

    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

    Loading discussion…