Catalog/VC/ShatterFunction/Contract.lean
| 1 | import Mathlib.Combinatorics.SetFamily.Shatter |
| 2 | |
| 3 | namespace Catalog.VC.ShatterFunction |
| 4 | |
| 5 | variable {ฮฑ : Type*} [DecidableEq ฮฑ] |
| 6 | |
| 7 | /-- The trace (restriction) of a set family `๐` on a subset `Y`: |
| 8 | the family `{ S โฉ Y | S โ ๐ }` of distinct intersections. -/ |
| 9 | def trace (๐ : Finset (Finset ฮฑ)) (Y : Finset ฮฑ) : Finset (Finset ฮฑ) := |
| 10 | ๐.image (ยท โฉ Y) |
| 11 | |
| 12 | /-- The primal shatter function `ฯ_๐(m)`: the maximum number of distinct |
| 13 | traces of `๐` on any `m`-element subset of the ground set. (Def 5.1) -/ |
| 14 | def shatterFun [Fintype ฮฑ] (๐ : Finset (Finset ฮฑ)) (m : โ) : โ := |
| 15 | (Finset.univ.filter (fun Y : Finset ฮฑ => Y.card = m)).sup |
| 16 | (fun Y => (trace ๐ Y).card) |
| 17 | |
| 18 | end Catalog.VC.ShatterFunction |
| 19 |