Lax Lean Archive

Scatter types

Lax185574.ScatterTypes · concepts/Lax185574/ScatterTypes.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 partial graph. A set S of vertices is r-scattered if all vertices of S have pairwise distance larger than r. Fix a linear order on V(G). For X ⊆ V(G) and r ∈ ℕ, S_r(X) is the inclusion-wise maximal r-scattered subset of X built by the greedy process that repeatedly adds the least available vertex.

    The (k, q)-scatter type stp^G_{k,q} is the function with domain

    {(r, tree_{k+i,q−i}(b)) | i ∈ [q], b ∈ V(G), r ∈ [9^{k+i} · ρ⁻(k+i, q−i)]}

    given by stp^G_{k,q}(r, ν) = min(|S_r([ν]^G)|, k + q). For q = 0 the domain is empty. A scatter type is represented canonically as the sorted list of its triples (r, ν, stp_{k,q}(r, ν)), using the canonical representation of ν. Its size ‖stp_{k,q}‖ is the size of this list.

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

    In the paper

    • page 45 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.TypeTrees
    2import Mathlib.Data.List.FinRange
    3
    4/-!
    5---
    6title: Scatter types
    7type: definition
    8---
    9Let G be a partial graph. A set S of vertices is *r-scattered* if all
    10vertices of S have pairwise distance larger than r. Fix a linear order
    11on V(G). For X ⊆ V(G) and r ∈ ℕ, S_r(X) is the inclusion-wise maximal
    12r-scattered subset of X built by the greedy process that repeatedly adds
    13the least available vertex.
    14
    15The *(k, q)-scatter type* stp^G_{k,q} is the function with domain
    16
    17 {(r, tree_{k+i,q−i}(b)) | i ∈ [q], b ∈ V(G),
    18 r ∈ [9^{k+i} · ρ⁻(k+i, q−i)]}
    19
    20given by stp^G_{k,q}(r, ν) = min(|S_r([ν]^G)|, k + q). For q = 0 the
    21domain is empty. A scatter type is represented canonically as the sorted
    22list of its triples (r, ν, stp_{k,q}(r, ν)), using the canonical
    23representation of ν. Its size ‖stp_{k,q}‖ is the size of this list.
    24
    25# Formalization notes
    26
    27The vertices are `Fin n`, ordered as numbers. The greedy process scans
    28the vertices in increasing order and adds a vertex of X when its
    29distance to every vertex added so far is larger than r. [k] = {1, …, k}
    30as in the paper, so i and r start at 1. The domain of stp^G_{k,q},
    31written domain(stp_{k,q}) in the paper, is `domain G k q`.
    32
    33The scatter type is given by its graph, the finite set of the pairs
    34((r, ν), stp_{k,q}(r, ν)) with (r, ν) in its domain. As a finite set it is
    35encoded as the sorted list of the words of these pairs, by
    36`Lax185574.Encodings`. The word of a pair is r, then the word of ν,
    37then the value.
    38-/
    39
    40namespace Lax185574.ScatterTypes
    41
    42open Lax185574.PartialGraphs Lax185574.GaifmanGraph
    43open Lax185574.TypeTrees
    44open Lax3.DistFO (rhoMinus rhoPlus)
    45
    46variable {n : ℕ}
    47
    48/-- `S_r(X)`: the greedy maximal `r`-scattered subset of `X`, scanning
    49the vertices in increasing order. -/
    50noncomputable def greedyScattered (G : PartialGraph (Fin n)) (r : ℕ) (X : Set (Fin n)) :
    51 List (Fin n) :=
    52 open Classical in
    53 (List.finRange n).foldl
    54 (fun S v => if v ∈ X ∧ ∀ u ∈ S, ¬ WithinDist G.resolved r u v then S ++ [v] else S) []
    55
    56/-- The domain `domain(stp_{k,q})` of the scatter type. -/
    57def domain (G : PartialGraph (Fin n)) (k q : ℕ) : Set (ℕ × TypeTree) :=
    58 {p | ∃ (i : ℕ) (b : Fin n), 1 ≤ i ∧ i ≤ q ∧ 1 ≤ p.1 ∧
    59 p.1 ≤ 9 ^ (k + i) * rhoMinus (k + i) (q - i) ∧
    60 p.2 = tree G (k + i) (q - i) ![b]}
    61
    62/-- The value `min(|S_r([ν]^G)|, k + q)` at the pair `p = (r, ν)`. -/
    63noncomputable def value (G : PartialGraph (Fin n)) (k q : ℕ) (p : ℕ × TypeTree) : ℕ :=
    64 min (greedyScattered G p.1 (realizations G p.2)).length (k + q)
    65
    66/-- The graph `{(x, f x) | x ∈ D}` of a function on a finite domain. -/
    67noncomputable def graphOn {α β : Type*} (D : Set α) (f : α → β) : Finset (α × β) :=
    68 finsetOf {p | p.1 ∈ D ∧ p.2 = f p.1}
    69
    70/-- `stp^G_{k,q}`, as its graph: the pairs `((r, ν), stp(r, ν))` with
    71`(r, ν) ∈ domain(stp_{k,q})`. -/
    72noncomputable def stp (G : PartialGraph (Fin n)) (k q : ℕ) : Finset ((ℕ × TypeTree) × ℕ) :=
    73 graphOn (domain G k q) (value G k q)
    74
    75end Lax185574.ScatterTypes
    76
    Formalization notes

    The vertices are FinnFin n, ordered as numbers. The greedy process scans the vertices in increasing order and adds a vertex of X when its distance to every vertex added so far is larger than r. [k] = {1, …, k} as in the paper, so i and r start at 1. The domain of stp^G_{k,q}, written domain(stp_{k,q}) in the paper, is domainGkqdomain G k q.

    The scatter type is given by its graph, the finite set of the pairs ((r, ν), stp_{k,q}(r, ν)) with (r, ν) in its domain. As a finite set it is encoded as the sorted list of the words of these pairs, by Lax185574.EncodingsLax185574.Encodings. The word of a pair is r, then the word of ν, then the value.

    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…