Research proof index

If a finite set family 𝒜 shatters a finite set s in the sense of Mathlib's Finset.Shatters, then the concept class of characteristic functions of sets in 𝒜 shatters ↑s in the sense of SetShatters. This bridges Mathlib's finset-based shattering to the predicate used by the PAC learning lower bounds.

Note that only the → direction needs the finiteness assumption.

Over a finite type, xs k is in InfOcc xs for all sufficiently large k.

Same as inf_acc_proj, but for pair types. This result does follow from inf_occ_proj, but that proof (see below) turns out to be longer.

Note that only the ⊇ direction needs the finiteness assumptions.

Given a set of strings all distinguishable by l (i.e., not related to each other by the Nerode congruence on l), the number of states in the DFA accepting l is at least the number of strings in the set.