Catalog/VC/DualShatterFunction/Full.lean
| 1 | import Mathlib.Combinatorics.SetFamily.Shatter |
| 2 | |
| 3 | namespace Catalog.VC.DualShatterFunction |
| 4 | |
| 5 | variable {ฮฑ : Type*} [DecidableEq ฮฑ] |
| 6 | |
| 7 | /-- The atom map of a subfamily `๐ด` at point `x`: the set of members |
| 8 | of `๐ด` that contain `x`. Two points `x, y` have the same atom map |
| 9 | iff they belong to exactly the same sets of `๐ด`. -/ |
| 10 | def atomMap (๐ด : Finset (Finset ฮฑ)) (x : ฮฑ) : Finset (Finset ฮฑ) := |
| 11 | ๐ด.filter (x โ ยท) |
| 12 | |
| 13 | /-- The dual shatter function `ฯ*_๐(m)`: the maximum number of distinct |
| 14 | atom types induced by any `m`-element subfamily of `๐`. |
| 15 | Equivalently, the maximum number of nonempty cells in the Venn diagram |
| 16 | of `m` sets chosen from `๐`. (Def 5.2) -/ |
| 17 | def dualShatterFun [Fintype ฮฑ] (๐ : Finset (Finset ฮฑ)) (m : โ) : โ := |
| 18 | (๐.powerset.filter (fun ๐ด => ๐ด.card = m)).sup |
| 19 | (fun ๐ด => (Finset.univ.image (atomMap ๐ด)).card) |
| 20 | |
| 21 | end Catalog.VC.DualShatterFunction |
| 22 |