Lax Lean Archive

Clustering of a tuple

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

    Let r ∈ ℕ, ℓ ≥ 1, G a graph and ā = (a₁, …, a_ℓ) ∈ V(G)^ℓ. There exist a radius ρ with r ≤ ρ ≤ 9^{ℓ−1} r and a partition 𝓑 of {a₁, …, a_ℓ} with the following property. For every X ⊆ V(G), every inclusion-wise maximal 4ρ-scattered subset S ⊆ X, and every H ≥ 4ρ + r,

    ∃x ∈ X: dist(x, ā) > r ⟺ ∃x ∈ X: r < dist(x, ā) ≤ H, or |{B ∈ 𝓑 | ∃x ∈ X: dist(x, B) ≤ r}| < |S|.

    Moreover, ρ and 𝓑 can be determined by tests of the form dist(aᵢ, aⱼ) ≤ s, where i, j ∈ [ℓ] and s ≤ 8 · 9^{ℓ−1} r.

    Concept map
    2 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 46 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.GaifmanGraph
    2import Mathlib.Data.Set.Card
    3
    4/-!
    5---
    6title: Clustering of a tuple
    7type: lemma
    8---
    9Let r ∈ ℕ, ℓ ≥ 1, G a graph and ā = (a₁, …, a_ℓ) ∈ V(G)^ℓ. There exist a
    10radius ρ with r ≤ ρ ≤ 9^{ℓ−1} r and a partition 𝓑 of {a₁, …, a_ℓ} with
    11the following property. For every X ⊆ V(G), every inclusion-wise
    12maximal 4ρ-scattered subset S ⊆ X, and every H ≥ 4ρ + r,
    13
    14 ∃x ∈ X: dist(x, ā) > r
    15 ⟺ ∃x ∈ X: r < dist(x, ā) ≤ H,
    16 or |{B ∈ 𝓑 | ∃x ∈ X: dist(x, B) ≤ r}| < |S|.
    17
    18Moreover, ρ and 𝓑 can be determined by tests of the form
    19dist(aᵢ, aⱼ) ≤ s, where i, j ∈ [ℓ] and s ≤ 8 · 9^{ℓ−1} r.
    20
    21# Formalization notes
    22
    23The paper cites Corollary 3.4 and Lemma 3.5 of its locality note. The
    24statement here makes "can be determined by tests" explicit by naming a
    25criterion that the tests decide. A radius ρ and a partition are
    26*admissible* if entries in the same block are within distance 4ρ − 2r
    27of each other, and entries in different blocks are not within distance
    284ρ + 2r. The statement says that an admissible pair with
    29r ≤ ρ ≤ 9^{ℓ−1} r exists, and that every admissible pair with r ≤ ρ has
    30the property above. Admissibility of a pair involves only tests
    31dist(aᵢ, aⱼ) ≤ s with s ≤ 4 · 9^{ℓ−1} r + 2r ≤ 8 · 9^{ℓ−1} r. So an
    32algorithm that knows these tests finds a suitable pair by trying all
    33candidates. A statement that only asserts that the pair is some
    34function of the tests would not let an algorithm compute it.
    35
    36The graph is finite. The partition is given on the positions: a function
    37β : [ℓ] → [ℓ] puts the positions i and j in the same block when
    38β(i) = β(j). dist(x, ā) > r means that x is within distance r of no
    39entry, and r < dist(x, ā) ≤ H means that x is within distance r of no
    40entry and within distance H of some entry.
    41-/
    42
    43namespace Lax185574.Clustering
    44
    45open Lax185574.GaifmanGraph
    46
    47variable {V : Type*}
    48
    49/-- The radius `ρ` and the partition `β` of the positions are
    50admissible for `a` at radius `r`: entries in one block are within
    51distance `4ρ − 2r`, and entries in different blocks are not within
    52distance `4ρ + 2r`. -/
    53def Admissible (G : SimpleGraph V) (r : ℕ) {ℓ : ℕ} (a : Fin ℓ → V) (ρ : ℕ)
    54 (β : Fin ℓ → Fin ℓ) : Prop :=
    55 ∀ i j, (β i = β j → WithinDist G (4 * ρ - 2 * r) (a i) (a j)) ∧
    56 (β i ≠ β j → ¬ WithinDist G (4 * ρ + 2 * r) (a i) (a j))
    57
    58/-- **Clustering.** Some admissible radius lies between `r` and
    59`9^(ℓ−1) r`, and every admissible pair detects the vertices of a set `X`
    60far from `a`: by vertices at bounded distance, or by counting a maximal
    61scattered subset of `X`. -/
    62axiom clustering [Finite V] (G : SimpleGraph V) (r ℓ : ℕ) (hℓ : 1 ≤ ℓ) (a : Fin ℓ → V) :
    63 (∃ ρ β, r ≤ ρ ∧ ρ ≤ 9 ^ (ℓ - 1) * r ∧ Admissible G r a ρ β) ∧
    64 ∀ ρ β, r ≤ ρ → Admissible G r a ρ β →
    65 ∀ (X S : Set V) (H : ℕ), S ⊆ X →
    66 (∀ x ∈ S, ∀ y ∈ S, x ≠ y → ¬ WithinDist G (4 * ρ) x y) →
    67 (∀ x ∈ X, ∃ y ∈ S, WithinDist G (4 * ρ) x y) →
    68 4 * ρ + r ≤ H →
    69 ((∃ x ∈ X, ∀ i, ¬ WithinDist G r (a i) x) ↔
    70 (∃ x ∈ X, (∀ i, ¬ WithinDist G r (a i) x) ∧ ∃ i, WithinDist G H (a i) x) ∨
    71 (β '' {i | ∃ x ∈ X, WithinDist G r (a i) x}).ncard < S.ncard)
    72
    73end Lax185574.Clustering
    74
    Show Proof
    Formalization notes

    The paper cites Corollary 3.4 and Lemma 3.5 of its locality note. The statement here makes "can be determined by tests" explicit by naming a criterion that the tests decide. A radius ρ and a partition are admissible if entries in the same block are within distance 4ρ − 2r of each other, and entries in different blocks are not within distance 4ρ + 2r. The statement says that an admissible pair with r ≤ ρ ≤ 9^{ℓ−1} r exists, and that every admissible pair with r ≤ ρ has the property above. Admissibility of a pair involves only tests dist(aᵢ, aⱼ) ≤ s with s ≤ 4 · 9^{ℓ−1} r + 2r ≤ 8 · 9^{ℓ−1} r. So an algorithm that knows these tests finds a suitable pair by trying all candidates. A statement that only asserts that the pair is some function of the tests would not let an algorithm compute it.

    The graph is finite. The partition is given on the positions: a function β : [ℓ] → [ℓ] puts the positions i and j in the same block when β(i) = β(j). dist(x, ā) > r means that x is within distance r of no entry, and r < dist(x, ā) ≤ H means that x is within distance r of no entry and within distance H of some entry.

    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…