feat(MachineLearning/PACLearning): definitions (#492)

Define the PAC learning model generalized to an arbitrary label type and
parameterized by a distribution family over labeled examples.

The unified definition `IsPACLearnerFor` captures the realizable,
agnostic, and noise-tolerant settings. Online PAC learning is not
treated here and left for future work. Given that the theorems we will
prove on this definition will require statements that look a whole lot
like `IsPACLearnerFor` anyways, this work will be compatible with future
online definitions.

---------

Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>

Author: SamuelSchlesinger

Cslib.lean

@@ -134,3 +134,4 @@ public import Cslib.Logics.Modal.Cube
 public import Cslib.Logics.Modal.Denotation
 public import Cslib.Logics.Propositional.Defs
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
+public import Cslib.MachineLearning.PACLearning.Defs