feat(MachineLearning/PACLearning): add VersionSpace abstraction

[Zetetic-Dhruv]

Adds the classical version space abstraction (Mitchell 1982, Angluin 1980) as a companion to the PAC learning definitions from #492.

• VersionSpace C S: the subset of C whose concepts agree with S on every sample point
• versionSpace_subset, versionSpace_empty_sample: sanity lemmas
• versionSpace_antitone: more data gives a smaller version space
• IsConsistent A C: predicate on learners whose output always lies in the version space
• mem_versionSpace_of_realizable, versionSpace_nonempty_of_realizable: realizable-case bridge

Foundation for downstream proofs (Sauer-Shelah, PAC lower bounds, infinite NFL).

[Zetetic-Dhruv]

@SamuelSchlesinger

[SamuelSchlesinger]

I want to see the bridge that makes this useful: version-space membership is exactly zero empirical error. I think that is what will motivate this PR and make the downstream work easier. The stuff you do have is sound and I appreciate this PR overall, my requests are mostly just stylistic commentary and generalization requests.

[Zetetic-Dhruv]

Hope the PR looks better now @SamuelSchlesinger

[SamuelSchlesinger]

It looks great, I think the last bit of the bridge is:

theorem empiricalError_eq_div [DecidableEq β] {m : ℕ} (hm : 0 < m)
      (h : α → β) (S : LabeledSample α β m) :
      empiricalError h S = (empiricalMiscount h S : ℝ≥0∞) / m

Would you implement that? Then it's good to go.

[Zetetic-Dhruv]

It looks great, I think the last bit of the bridge is:

theorem empiricalError_eq_div [DecidableEq β] {m : ℕ} (hm : 0 < m)
      (h : α → β) (S : LabeledSample α β m) :
      empiricalError h S = (empiricalMiscount h S : ℝ≥0∞) / m

Would you implement that? Then it's good to go.

Hey, done as you suggested, sorry for missing this!

[Zetetic-Dhruv]

✔ [126/126] Built mk_all:exe (988ms)
The file 'Cslib.lean' is out of date: run lake exe mk_all to update it
Error: Process completed with exit code 1.

Source of error in action

[Zetetic-Dhruv]

Regenerated cslib.lean. Can someone rerun the ci-check?

[SamuelSchlesinger]

@fmontesi whenever you'd like, we can merge this.

[fmontesi]

Excellent, thank you!