Lax Lean Archive

Pairs at distance at most 5 in both polarities

Lax185574.PairRelation · concepts/Lax185574/PairRelation.lean · lax-185574

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

    Let G be a graph and 𝒫 a partition of V = V(G). Define R = R(G, 𝒫) ⊆ (V choose 2) so that for all parts X, Y ∈ 𝒫 (possibly X = Y) and pairs uv with u ∈ X, v ∈ Y and u ≠ v, we have uv ∈ R if and only if

    dist^{G[X,Y]}(u, v) ≤ 5 and dist^{Ḡ[X,Y]}(u, v) ≤ 5.

    Concept map
    9 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 33 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.BipartiteGraphs
    2import Lax185574.Partitions
    3import Lax185574.GaifmanGraph
    4
    5/-!
    6---
    7title: Pairs at distance at most 5 in both polarities
    8type: definition
    9---
    10Let G be a graph and 𝒫 a partition of V = V(G). Define
    11R = R(G, 𝒫) ⊆ (V choose 2) so that for all parts X, Y ∈ 𝒫 (possibly
    12X = Y) and pairs uv with u ∈ X, v ∈ Y and u ≠ v, we have uv ∈ R if and
    13only if
    14
    15dist^{G[X,Y]}(u, v) ≤ 5 and dist^{Ḡ[X,Y]}(u, v) ≤ 5.
    16
    17# Formalization notes
    18
    19The relation is a simple graph on V. For a pair uv the parts are
    20X = 𝒫(u) and Y = 𝒫(v), and the distances are those from the left copy of
    21u to the right copy of v in the graphs `pairGraph G X Y` and
    22`coPairGraph G X Y` of `Lax185574.BipartiteGraphs`, measured by walks.
    23When X = Y the vertices u and v lie in opposite copies of X, as in the
    24paper. `SimpleGraph.fromRel` removes the pairs with u = v and
    25symmetrizes. The condition is already symmetric in u and v, since
    26exchanging the two copies of V maps G[X, Y] to G[Y, X].
    27-/
    28
    29namespace Lax185574.PairRelation
    30
    31open Lax185574.BipartiteGraphs Lax185574.Partitions Lax185574.GaifmanGraph
    32
    33universe z
    34
    35variable {V : Type z}
    36
    37/-- The relation `R(G, 𝒫)`: distinct `u` and `v` are related if they
    38are within distance `5` both in `G[𝒫(u), 𝒫(v)]` and in
    39`Ḡ[𝒫(u), 𝒫(v)]`. -/
    40def pairRelation (G : SimpleGraph V) (P : Setoid V) : SimpleGraph V :=
    41 SimpleGraph.fromRel fun u v =>
    42 WithinDist (pairGraph G (part P u) (part P v)) 5 (.inl u) (.inr v) ∧
    43 WithinDist (coPairGraph G (part P u) (part P v)) 5 (.inl u) (.inr v)
    44
    45end Lax185574.PairRelation
    46
    Formalization notes

    The relation is a simple graph on V. For a pair uv the parts are X = 𝒫(u) and Y = 𝒫(v), and the distances are those from the left copy of u to the right copy of v in the graphs pairGraphGXYpairGraph G X Y and coPairGraphGXYcoPairGraph G X Y of Lax185574.BipartiteGraphsLax185574.BipartiteGraphs, measured by walks. When X = Y the vertices u and v lie in opposite copies of X, as in the paper. SimpleGraph.fromRelSimpleGraph.fromRel removes the pairs with u = v and symmetrizes. The condition is already symmetric in u and v, since exchanging the two copies of V maps G[X, Y] to G[Y, X].

    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…