Catalog/VC/VCDimension/Full.lean
| 1 | import Mathlib.Combinatorics.SetFamily.Shatter |
| 2 | |
| 3 | namespace Catalog.VC.VCDimension |
| 4 | |
| 5 | /-- A finite set `s` is shattered by family `𝒜` if every subset of `s` |
| 6 | is realized as `s ∩ S` for some `S ∈ 𝒜`. |
| 7 | Wraps Mathlib's `Finset.Shatters`. (Def 5.8) -/ |
| 8 | abbrev Shatters {α : Type*} [DecidableEq α] |
| 9 | (𝒜 : Finset (Finset α)) (s : Finset α) : Prop := |
| 10 | 𝒜.Shatters s |
| 11 | |
| 12 | /-- The VC-dimension of `𝒜`: the maximum cardinality of a set shattered |
| 13 | by `𝒜`. Equivalently, `sup { m : π_𝒜(m) = 2^m }`. |
| 14 | Wraps Mathlib's `Finset.vcDim`. (Def 5.8) -/ |
| 15 | abbrev vcDim {α : Type*} [DecidableEq α] |
| 16 | (𝒜 : Finset (Finset α)) : ℕ := |
| 17 | 𝒜.vcDim |
| 18 | |
| 19 | end Catalog.VC.VCDimension |
| 20 |