Lax Lean Archive

Neighborhood complexity and VC-dimension

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

    The neighborhood complexity of a graph G is the function π_G : ℕ → ℕ defined by

    π_G(k) ≔ max_{S ⊆ V(G), |S| ≤ k} |{ N^G(v) ∩ S : v ∈ V(G) }|,

    which counts the maximum number of distinct neighborhoods of vertices of G restricted to a set of size at most k.

    The VC-dimension of a graph G is the maximal size of a set A ⊆ V(G) such that { N(v) ∩ A : v ∈ V(G) } = 2^A.

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

    In the paper

    • page 13 of this submission's paper

    Lean source view on GitHub

    1import Lax199508.NeighborhoodComplexity
    2import Mathlib.Data.ENat.Lattice
    3
    4/-!
    5---
    6title: Neighborhood complexity and VC-dimension
    7type: definition
    8---
    9The *neighborhood complexity* of a graph G is the function π_G : ℕ → ℕ
    10defined by
    11
    12π_G(k) ≔ max_{S ⊆ V(G), |S| ≤ k} |{ N^G(v) ∩ S : v ∈ V(G) }|,
    13
    14which counts the maximum number of distinct neighborhoods of vertices of
    15G restricted to a set of size at most k.
    16
    17The *VC-dimension* of a graph G is the maximal size of a set A ⊆ V(G)
    18such that { N(v) ∩ A : v ∈ V(G) } = 2^A.
    19
    20# Formalization notes
    21
    22The number of traces |{ N^G(v) ∩ S : v ∈ V(G) }| is `traceCount` of the
    23Sparsity Lectures submission (Lax199508), which is the cardinality of
    24the set of traces. For a finite set S the traces are subsets of S, so
    25there are at most 2^|S| of them and the count is exact. The maximum over
    26all S with |S| ≤ k is the supremum of a set of natural numbers bounded
    27by 2^k, so it is attained.
    28
    29A set A is shattered if every subset B ⊆ A is the trace N(v) ∩ A of some
    30vertex v. The VC-dimension is the supremum of the sizes of the finite
    31shattered sets, an extended natural number. It is the maximum of the
    32paper whenever that exists, and ⊤ for a graph with arbitrarily large
    33shattered sets. "VC-dimension at most d" is `vcDim G ≤ d`.
    34-/
    35
    36namespace Lax185574.VCDimension
    37
    38open Lax199508.NeighborhoodComplexity
    39
    40universe u
    41
    42variable {V : Type u}
    43
    44/-- The neighborhood complexity `π_G(k)`: the largest number of
    45neighborhood traces `N(v) ∩ S` on a set `S` of at most `k` vertices. -/
    46noncomputable def neighborhoodComplexity (G : SimpleGraph V) (k : ℕ) : ℕ :=
    47 sSup {m | ∃ S : Finset V, S.card ≤ k ∧ m = traceCount G (S : Set V)}
    48
    49/-- The neighborhoods of `G` shatter `A`: every subset of `A` is the
    50trace `N(v) ∩ A` of some vertex `v`. -/
    51def Shatters (G : SimpleGraph V) (A : Finset V) : Prop :=
    52 ∀ B ⊆ A, ∃ v : V, ∀ a ∈ A, (G.Adj v a ↔ a ∈ B)
    53
    54/-- The VC-dimension of `G`: the supremum of the sizes of the finite
    55vertex sets shattered by the neighborhoods. -/
    56noncomputable def vcDim (G : SimpleGraph V) : ℕ∞ :=
    57 ⨆ (A : Finset V) (_ : Shatters G A), (A.card : ℕ∞)
    58
    59end Lax185574.VCDimension
    60
    Formalization notes

    The number of traces |{ N^G(v) ∩ S : v ∈ V(G) }| is traceCounttraceCount of the Sparsity Lectures submission (Lax199508), which is the cardinality of the set of traces. For a finite set S the traces are subsets of S, so there are at most 2^|S| of them and the count is exact. The maximum over all S with |S| ≤ k is the supremum of a set of natural numbers bounded by 2^k, so it is attained.

    A set A is shattered if every subset B ⊆ A is the trace N(v) ∩ A of some vertex v. The VC-dimension is the supremum of the sizes of the finite shattered sets, an extended natural number. It is the maximum of the paper whenever that exists, and ⊤ for a graph with arbitrarily large shattered sets. "VC-dimension at most d" is vcDimG≤dvcDim G ≤ d.

    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…