Lax Lean Archive

Bounded VC-dimension of monadically dependent classes

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

    Observation

    For every monadically dependent graph class 𝒞 there is some d ∈ ℕ such that every graph G ∈ 𝒞 has VC-dimension at most d.

    The paper notes that this is easy to see from the definition of monadic dependence, and refers to the companion paper for a proof.

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

    Lean source view on GitHub

    1import Lax185574.VCDimension
    2import Lax185574.MonadicDependence
    3
    4/-!
    5---
    6title: Bounded VC-dimension of monadically dependent classes
    7type: observation
    8---
    9For every monadically dependent graph class 𝒞 there is some d ∈ ℕ such
    10that every graph G ∈ 𝒞 has VC-dimension at most d.
    11
    12The paper notes that this is easy to see from the definition of monadic
    13dependence, and refers to the companion paper for a proof.
    14
    15# Formalization notes
    16
    17The VC-dimension is that of `Lax185574.VCDimension`, an extended natural
    18number, and "VC-dimension at most d" is `vcDim G.toSimpleGraph ≤ d`. The
    19paper allows infinite graphs in this part. Here the graphs are those of
    20a `GraphClass`, which are finite, as in every use.
    21
    22The constant d is chosen after 𝒞 and before the graph. Monadic
    23dependence is that of `Lax185574.MonadicDependence`, by transductions.
    24By `Lax185574.IndependenceProperty` no formula has the independence
    25property on a monadically dependent class, from which the observation
    26is immediate: a class whose graphs have unbounded VC-dimension gives the
    27edge formula the independence property.
    28-/
    29
    30namespace Lax185574.BoundedVCClasses
    31
    32open Lax185574.Graphs Lax185574.MonadicDependence Lax185574.VCDimension
    33
    34/-- **Bounded VC-dimension.** Some `d` bounds the VC-dimension of every
    35graph of a monadically dependent class. -/
    36axiom exists_vcDim_le (C : GraphClass) (hC : MonadicallyDependent C) :
    37 ∃ d : ℕ, ∀ G ∈ C, vcDim G.toSimpleGraph ≤ d
    38
    39end Lax185574.BoundedVCClasses
    40
    Show Proof
    Formalization notes

    The VC-dimension is that of Lax185574.VCDimensionLax185574.VCDimension, an extended natural number, and "VC-dimension at most d" is vcDimG.toSimpleGraph≤dvcDim G.toSimpleGraph ≤ d. The paper allows infinite graphs in this part. Here the graphs are those of a GraphClassGraphClass, which are finite, as in every use.

    The constant d is chosen after 𝒞 and before the graph. Monadic dependence is that of Lax185574.MonadicDependenceLax185574.MonadicDependence, by transductions. By Lax185574.IndependencePropertyLax185574.IndependenceProperty no formula has the independence property on a monadically dependent class, from which the observation is immediate: a class whose graphs have unbounded VC-dimension gives the edge formula the independence property.

    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…