Lax Lean Archive

Few types far from a parameter set

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

proven

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

    Lemma

    For every q, k, c ∈ ℕ there are numbers r = r(q) and T = T(q, k, c) with the following property. Let H be a graph expanded by at most c unary predicates and U ⊆ V(H). Consider the set

    F ≔ { a ∈ V(H) : dist^H(a, U) > r }

    of vertices that are far from U. Then |Types^H_{k,q}(F/U)| ≤ T(q, k, c).

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 63 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.Colorings
    2import Lax185574.FirstOrderTypes
    3import Lax185574.GraphBalls
    4
    5/-!
    6---
    7title: Few types far from a parameter set
    8type: lemma
    9---
    10For every q, k, c ∈ ℕ there are numbers r = r(q) and T = T(q, k, c)
    11with the following property. Let H be a graph expanded by at most c
    12unary predicates and U ⊆ V(H). Consider the set
    13
    14 F ≔ { a ∈ V(H) : dist^H(a, U) > r }
    15
    16of vertices that are far from U. Then |Types^H_{k,q}(F/U)| ≤ T(q, k, c).
    17
    18# Formalization notes
    19
    20The radius r is quantified after q and before k and c, and T after
    21q, k and c. In particular neither depends on the graph or on |U|. An
    22expansion by at most c unary predicates is an expansion by exactly c
    23color sets, some of which may be empty, as in `Colorings.expansion`.
    24The graph is finite, which is the case in which the lemma is used. The
    25distance is that of the graph H, which is also the distance in the
    26Gaifman graph of the expansion. The far set F is the complement of
    27the ball Ball^H_r[U] of `GraphBalls.graphBall`, so a vertex lies in F if
    28no walk of length at most r joins a vertex of U to it. If U is empty, F
    29is the whole vertex set.
    30-/
    31
    32namespace Lax185574.SeparatingTypes
    33
    34open FirstOrder FirstOrder.Language Lax710763.Transductions
    35open Lax185574.FirstOrderTypes Lax185574.GraphBalls Lax185574.Colorings
    36
    37universe z
    38
    39/-- **Few types far from a parameter set.** In a graph with `c` unary
    40predicates, the `k`-tuples of vertices at distance more than `r(q)` from
    41`U` realize at most `T(q, k, c)` types of quantifier rank `q` over
    42`U`. -/
    43axiom typeCountOver_far_le (q : ℕ) :
    44 ∃ r : ℕ, ∀ k c : ℕ, ∃ T : ℕ,
    45 ∀ (V : Type z) [Finite V] (G : SimpleGraph V) (colors : Fin c → Set V)
    46 (U : Set V),
    47 @typeCountOver (withColors Language.graph c) V (expansion G colors) k q
    48 (graphBall G r U)ᶜ U ≤ T
    49
    50end Lax185574.SeparatingTypes
    51
    Show Proof
    Formalization notes

    The radius r is quantified after q and before k and c, and T after q, k and c. In particular neither depends on the graph or on |U|. An expansion by at most c unary predicates is an expansion by exactly c color sets, some of which may be empty, as in Colorings.expansionColorings.expansion. The graph is finite, which is the case in which the lemma is used. The distance is that of the graph H, which is also the distance in the Gaifman graph of the expansion. The far set F is the complement of the ball Ball^H_r[U] of GraphBalls.graphBallGraphBalls.graphBall, so a vertex lies in F if no walk of length at most r joins a vertex of U to it. If U is empty, F is the whole vertex set.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…