feat(MachineLearning/PACLearning): realizable distribution family

[LibertasSpZ]

• Contents:

  • define realizable distributions for downstream formalization of realizable PAC learning concepts and results. For a concept class C, a distribution D on α × β is realizable by C when some concept in C has zero true error under D.
    • For discrete label types such as β = Bool, this family contains the pushforward family described in Defs.lean; an inclusion lemma, under the measurability hypotheses error_map_eq_hypothesisError already uses, is a natural follow-up.
    • The zero-error formulation is the natural one once labels come from a joint distribution (ShalevShwartzBenDavid2014 §3.2.1): it is defined solely through error and needs no marginal, graph map, or measurability hypothesis, whereas the pushforward formulation can fail to yield zero error without the measurability hypotheses above.
  • formalize some basic properties such as monotonicity and zero optimal error for realizable distributions.

• Next steps:

  • formalize more results about realizable PAC learning.

• AI disclosure:

  • used Claude Fable (5, 5.1) for literature research, design discussion and code setup; used GPT-5.6-sol for proof completion.
  • All definitions, statements, and proofs were reviewed and verified by me.