Lax Lean Archive

The far tree

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

    For a partial graph G, k ∈ ℕ, q ≥ 1 and a nonempty tuple ā of at most k vertices,

    ftree_{k,q}(ā) = {tree_{k+1,q−1}(b) | b ∈ V(G), dist(ā, b) > ρ⁻(k+1, q−1)}.

    It is the set of type trees of the vertices far from ā.

    Concept map
    12 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 46 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.TypeTrees
    2
    3/-!
    4---
    5title: The far tree
    6type: definition
    7---
    8For a partial graph G, k ∈ ℕ, q ≥ 1 and a nonempty tuple ā of at most k
    9vertices,
    10
    11 ftree_{k,q}(ā) = {tree_{k+1,q−1}(b) | b ∈ V(G), dist(ā, b) > ρ⁻(k+1, q−1)}.
    12
    13It is the set of type trees of the vertices far from ā.
    14
    15# Formalization notes
    16
    17dist(ā, b) > r means that no entry of ā is within distance r of b. The
    18far tree is a finite set of type trees. It is encoded as the sorted list
    19of the words of its trees, like the sets inside a type tree.
    20-/
    21
    22namespace Lax185574.FarTrees
    23
    24open Lax185574.PartialGraphs Lax185574.GaifmanGraph
    25open Lax185574.TypeTrees
    26open Lax3.DistFO (rhoMinus rhoPlus)
    27
    28variable {V : Type*}
    29
    30/-- `ftree_{k,q}(a)`: the type trees of the vertices far from `a`. -/
    31noncomputable def ftree (G : PartialGraph V) (k q : ℕ) {ℓ : ℕ} (a : Fin ℓ → V) :
    32 Finset TypeTree :=
    33 finsetOf {ν | ∃ b : V,
    34 (∀ i, ¬ WithinDist G.resolved (rhoMinus (k + 1) (q - 1)) (a i) b) ∧
    35 ν = tree G (k + 1) (q - 1) ![b]}
    36
    37end Lax185574.FarTrees
    38
    Formalization notes

    dist(ā, b) > r means that no entry of ā is within distance r of b. The far tree is a finite set of type trees. It is encoded as the sorted list of the words of its trees, like the sets inside a type tree.

    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…