Commit 2023-11-14 03:24 0a0580ba

View on Github →

feat: Shattering (#7524) Define when a finset family shatters a finset, the shatterer of a finset, define the Vapnik-Chervonenkis dimension of a finset family and prove the Sauer-Shelah lemma

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SetFamily/Shatter.lean

added theorem Finset.Shatters.card_le_vcDim

added theorem Finset.Shatters.exists_inter_eq_singleton

added theorem Finset.Shatters.exists_superset

added theorem Finset.Shatters.mono_left

added theorem Finset.Shatters.mono_right

added theorem Finset.Shatters.of_compression

added def Finset.Shatters

added theorem Finset.card_le_card_shatterer

added theorem Finset.card_shatterer_le_sum_vcDim

added theorem Finset.isLowerSet_shatterer

added theorem Finset.mem_shatterer

added def Finset.shatterer

added theorem Finset.shatterer_compress_subset_shatterer

added theorem Finset.shatterer_eq

added theorem Finset.shatterer_idem

added theorem Finset.shatterer_mono

added theorem Finset.shatters_empty

added theorem Finset.shatters_iff

added theorem Finset.shatters_of_forall_subset

added theorem Finset.shatters_shatterer

added theorem Finset.shatters_univ

added theorem Finset.subset_shatterer

added theorem Finset.univ_shatters

added def Finset.vcDim

added theorem Finset.vcDim_compress_le