Lax Lean Archive

Chains and their radius-r width

Lax185574.Chains · concepts/Lax185574/Chains.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

    A chain in a graph G is a decreasing sequence V(G) = S₁ ⊇ ⋯ ⊇ S_ℓ = ∅ of vertex sets. Its radius-r width, for r ∈ ℕ, is

    max_{2 ≤ i ≤ ℓ} max_{v ∈ V(G)} |ATypes^G(Ball_r^{S_i}(v)/S_{i−1})| = max_{2 ≤ i ≤ ℓ} max_{v ∈ V(G)} |Ball_r^{S_i}(v)/𝒫_{S_{i−1}}|,

    where Ball_r^S(v) is the ball in the metric of S-flips and 𝒫_S is the partition into atomic types over S.

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

    In the paper

    • page 30 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.Flips
    2import Mathlib.Order.Lattice.Nat
    3
    4/-!
    5---
    6title: Chains and their radius-r width
    7type: definition
    8---
    9A *chain* in a graph G is a decreasing sequence
    10V(G) = S₁ ⊇ ⋯ ⊇ S_ℓ = ∅ of vertex sets. Its *radius-r width*, for
    11r ∈ ℕ, is
    12
    13max_{2 ≤ i ≤ ℓ} max_{v ∈ V(G)} |ATypes^G(Ball_r^{S_i}(v)/S_{i−1})|
    14 = max_{2 ≤ i ≤ ℓ} max_{v ∈ V(G)} |Ball_r^{S_i}(v)/𝒫_{S_{i−1}}|,
    15
    16where Ball_r^S(v) is the ball in the metric of S-flips and 𝒫_S is the
    17partition into atomic types over S.
    18
    19# Formalization notes
    20
    21The formalization lists a chain in the reverse order, as the increasing
    22sequence ∅ = S₁ ⊆ ⋯ ⊆ S_ℓ = V(G). A chain is a nonempty list of finite
    23vertex sets, the first empty, the last the whole vertex set, and each
    24contained in the next. Consecutive sets may be equal. Reversing the list
    25turns a chain of the paper into one of the formalization, and the
    26widths agree after the reversal. A term of the paper pairs a set with
    27its predecessor, which is the larger set: the ball is taken in the
    28metric of flips of the smaller set, and the partition into atomic types
    29over the larger one. In the formalization the term for consecutive sets
    30S_t ⊆ S_{t+1} takes the ball in the metric of S_t-flips and the
    31partition 𝒫_{S_{t+1}}, which is the same term.
    32
    33The width is the second form of the paper: the number of parts of
    34the partition into atomic types that meet the ball. The vertices of the
    35ball with the same atomic type over a set S are exactly those in the
    36same part of 𝒫_S, so the two forms agree. The maximum is the supremum of a set of natural numbers,
    37finite on a finite vertex type. The empty maximum, for a chain of length
    38one, is 0.
    39
    40The chain is the same object for every graph on the vertex set. The
    41graph enters only the width.
    42-/
    43
    44namespace Lax185574.Chains
    45
    46open Lax185574.Partitions Lax185574.Flips
    47
    48universe z
    49
    50variable {V : Type z}
    51
    52/-- `S` is a chain: `∅ = S₁ ⊆ ⋯ ⊆ S_m = V`. -/
    53def IsChain [Fintype V] (S : List (Finset V)) : Prop :=
    54 ∃ h : S ≠ [], S.head h = ∅ ∧ S.getLast h = Finset.univ ∧
    55 ∀ (t : ℕ) (ht : t + 1 < S.length), S[t] ⊆ S[t + 1]
    56
    57/-- The radius-`r` width of the chain `S` in `G`: the largest number of
    58parts of `𝒫_{S_{t+1}}` that meet a radius-`r` ball in the metric of
    59`S_t`-flips. -/
    60noncomputable def chainWidth (G : SimpleGraph V) (r : ℕ) (S : List (Finset V)) : ℕ :=
    61 sSup {K | ∃ (t : ℕ) (ht : t + 1 < S.length) (v : V),
    62 K = partCount (atomicTypes G (S[t + 1] : Set V))
    63 (flipBall G (atomicTypes G (S[t] : Set V)) r v)}
    64
    65end Lax185574.Chains
    66
    Formalization notes

    The formalization lists a chain in the reverse order, as the increasing sequence ∅ = S₁ ⊆ ⋯ ⊆ S_ℓ = V(G). A chain is a nonempty list of finite vertex sets, the first empty, the last the whole vertex set, and each contained in the next. Consecutive sets may be equal. Reversing the list turns a chain of the paper into one of the formalization, and the widths agree after the reversal. A term of the paper pairs a set with its predecessor, which is the larger set: the ball is taken in the metric of flips of the smaller set, and the partition into atomic types over the larger one. In the formalization the term for consecutive sets S_t ⊆ S_{t+1} takes the ball in the metric of S_t-flips and the partition 𝒫_{S_{t+1}}, which is the same term.

    The width is the second form of the paper: the number of parts of the partition into atomic types that meet the ball. The vertices of the ball with the same atomic type over a set S are exactly those in the same part of 𝒫_S, so the two forms agree. The maximum is the supremum of a set of natural numbers, finite on a finite vertex type. The empty maximum, for a chain of length one, is 0.

    The chain is the same object for every graph on the vertex set. The graph enters only the width.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…