Skip to content

Commit 45072a3

Browse files
Zetetic-Dhruvdhruvgupta-zetesisfmontesi
authored
feat(MachineLearning/PACLearning): add VersionSpace abstraction (#592)
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). --------- Co-authored-by: dhruvgupta-zetesis <dhruv.gupta@artpark.in> Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>
1 parent 00ecf15 commit 45072a3

3 files changed

Lines changed: 350 additions & 0 deletions

File tree

‎Cslib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -140,4 +140,5 @@ public import Cslib.Logics.Propositional.Defs
140140
public import Cslib.Logics.Propositional.NaturalDeduction.Basic
141141
public import Cslib.MachineLearning.PACLearning.Defs
142142
public import Cslib.MachineLearning.PACLearning.VCDimension
143+
public import Cslib.MachineLearning.PACLearning.VersionSpace
143144
public import Cslib.Probability.PMF

‎Cslib/MachineLearning/PACLearning/VersionSpace.lean‎

Lines changed: 310 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,310 @@
1+
/-
2+
Copyright (c) 2026 Dhruv Gupta. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Dhruv Gupta
5+
-/
6+
7+
module
8+
9+
public import Cslib.MachineLearning.PACLearning.Defs
10+
public import Mathlib.MeasureTheory.Measure.Dirac
11+
public import Mathlib.MeasureTheory.Measure.Map
12+
13+
/-! # Version Space
14+
15+
The *version space* of a concept class `C` given a labeled sample `S` is the
16+
subset of `C` whose concepts agree with `S` on every observed point — the
17+
classical "concepts still consistent with the data" of Mitchell (1977) and
18+
Angluin (1980).
19+
20+
## Main definitions
21+
22+
- `VersionSpace C S`: the subset of `C` whose concepts agree with `S` on every
23+
sample point.
24+
- `IsConsistent A C`: a learner is consistent with `C` if its output always lies
25+
in the version space at the received sample.
26+
- `empiricalMiscount h S`: number of sample points where `h` errs (`[DecidableEq β]`).
27+
- `empiricalMeasure S`: the uniform Dirac mixture over the sample.
28+
- `empiricalError h S`: the empirical distribution's mass on the disagreement set.
29+
- `Realizable C S`: some concept in `C` labels every sample point correctly.
30+
31+
## Main results
32+
33+
- `versionSpace_subset`, `versionSpace_empty_sample`, `versionSpace_reindex`,
34+
`versionSpace_antitone`, `versionSpace_mono_C`: structural properties.
35+
- `mem_versionSpace_iff_empiricalMiscount_zero`: combinatorial bridge.
36+
- `mem_versionSpace_iff_empiricalError_zero`: measure-theoretic bridge.
37+
- `IsConsistent.empiricalMiscount_eq_zero`, `IsConsistent.empiricalError_eq_zero`:
38+
consistent learners achieve zero error / miscount on every sample.
39+
- `mem_versionSpace_of_realizable`, `Realizable.versionSpace_nonempty`: realizable
40+
samples give non-empty version spaces.
41+
- `ae_mem_versionSpace_of_realizable`: under iid sampling from a realizable
42+
joint distribution, the target concept lies in the version space almost surely.
43+
44+
## References
45+
46+
* [Mitchell1977]
47+
* [Mitchell1982]
48+
* [Angluin1980]
49+
* [Mitchell1997]
50+
-/
51+
52+
@[expose] public section
53+
54+
open MeasureTheory Set
55+
open scoped ENNReal
56+
57+
namespace Cslib.MachineLearning.PACLearning
58+
59+
variable {α : Type*} {β : Type*}
60+
61+
/-! ### Version Space -/
62+
63+
/-- The *version space* of a concept class `C` given a labeled sample `S`:
64+
the set of concepts in `C` whose labels agree with `S` on every observed point. -/
65+
def VersionSpace {m : ℕ} (C : ConceptClass α β) (S : LabeledSample α β m) :
66+
ConceptClass α β :=
67+
{h ∈ C | ∀ i : Fin m, h (S i).1 = (S i).2}
68+
69+
/-- Membership in the version space unfolds to concept membership plus
70+
per-sample consistency. -/
71+
theorem mem_versionSpace_iff {m : ℕ} {C : ConceptClass α β}
72+
{S : LabeledSample α β m} {h : α → β} :
73+
h ∈ VersionSpace C S ↔ h ∈ C ∧ ∀ i : Fin m, h (S i).1 = (S i).2 := Iff.rfl
74+
75+
/-- The version space is a subset of the original concept class. -/
76+
theorem versionSpace_subset {m : ℕ} (C : ConceptClass α β)
77+
(S : LabeledSample α β m) :
78+
VersionSpace C S ⊆ C := fun _ hh => hh.1
79+
80+
/-- Version space on the empty sample equals the whole concept class. -/
81+
theorem versionSpace_empty_sample (C : ConceptClass α β)
82+
(S : LabeledSample α β 0) :
83+
VersionSpace C S = C := by
84+
ext h
85+
refine ⟨fun hh => hh.1, fun hh => ⟨hh, fun i => i.elim0⟩⟩
86+
87+
/-- *Version space reindexing.* For any reindexing `f : Fin m → Fin n`, the
88+
version space on `S` is contained in the version space on the reindexed sample
89+
`S ∘ f`. -/
90+
theorem versionSpace_reindex {m n : ℕ} (f : Fin m → Fin n) (C : ConceptClass α β)
91+
(S : LabeledSample α β n) :
92+
VersionSpace C S ⊆ VersionSpace C (S ∘ f) :=
93+
fun _ hh => ⟨hh.1, fun i => hh.2 (f i)⟩
94+
95+
/-- *Version space antitonicity.* Given a sample of size `n` and `m ≤ n`, the
96+
version space on all `n` observations is a subset of the version space on the
97+
first `m` observations. Special case of `versionSpace_reindex` with
98+
`f := Fin.castLE hmn`. -/
99+
theorem versionSpace_antitone {m n : ℕ} (hmn : m ≤ n) (C : ConceptClass α β)
100+
(S : LabeledSample α β n) :
101+
VersionSpace C S ⊆ VersionSpace C (S ∘ Fin.castLE hmn) :=
102+
versionSpace_reindex (Fin.castLE hmn) C S
103+
104+
/-- *Version space is monotone in the concept class.* -/
105+
theorem versionSpace_mono_C {m : ℕ} {C C' : ConceptClass α β} (hCC' : C ⊆ C')
106+
(S : LabeledSample α β m) :
107+
VersionSpace C S ⊆ VersionSpace C' S :=
108+
fun _ hh => ⟨hCC' hh.1, hh.2⟩
109+
110+
/-! ### Empirical Error -/
111+
112+
/-- The *empirical miscount* of a hypothesis `h` on a labeled sample `S`: the
113+
number of sample points where `h` predicts incorrectly. -/
114+
def empiricalMiscount [DecidableEq β] {m : ℕ} (h : α → β)
115+
(S : LabeledSample α β m) : ℕ :=
116+
(Finset.univ.filter fun i : Fin m => h (S i).1 ≠ (S i).2).card
117+
118+
section EmpiricalMeasure
119+
variable [MeasurableSpace α] [MeasurableSpace β]
120+
121+
/-- The *empirical distribution* of a labeled sample: the uniform mixture of
122+
Dirac measures at each sample point. Equals the zero measure when `m = 0`. -/
123+
noncomputable def empiricalMeasure {m : ℕ} (S : LabeledSample α β m) :
124+
Measure (α × β) :=
125+
if _hm : m = 0 then 0
126+
else (m : ℝ≥0∞)⁻¹ • ∑ i, Measure.dirac (S i)
127+
128+
/-- The *empirical 0-1 error* of `h` on `S`: the empirical distribution's
129+
mass on the disagreement set. -/
130+
noncomputable def empiricalError {m : ℕ} (h : α → β) (S : LabeledSample α β m) :
131+
ℝ≥0∞ :=
132+
error (empiricalMeasure S) h
133+
134+
end EmpiricalMeasure
135+
136+
/-- Version-space membership equals concept-class membership plus zero empirical
137+
miscount (combinatorial bridge). -/
138+
theorem mem_versionSpace_iff_empiricalMiscount_zero [DecidableEq β]
139+
{m : ℕ} {C : ConceptClass α β} {S : LabeledSample α β m} {h : α → β} :
140+
h ∈ VersionSpace C S ↔ h ∈ C ∧ empiricalMiscount h S = 0 := by
141+
simp only [empiricalMiscount, Finset.card_eq_zero, Finset.filter_eq_empty_iff,
142+
Finset.mem_univ, true_implies, ne_eq, Decidable.not_not]
143+
rfl
144+
145+
/-- Version-space membership equals concept-class membership plus zero empirical
146+
error (measure-theoretic bridge). -/
147+
theorem mem_versionSpace_iff_empiricalError_zero
148+
[MeasurableSpace α] [MeasurableSpace β]
149+
[MeasurableSingletonClass α] [MeasurableSingletonClass β]
150+
{m : ℕ} {C : ConceptClass α β} {S : LabeledSample α β m} {h : α → β} :
151+
h ∈ VersionSpace C S ↔ h ∈ C ∧ empiricalError h S = 0 := by
152+
refine and_congr_right fun _ => ?_
153+
unfold empiricalError empiricalMeasure error
154+
rcases Nat.eq_zero_or_pos m with hm | hm
155+
· subst hm
156+
rw [dif_pos rfl]
157+
simp only [Measure.coe_zero, Pi.zero_apply]
158+
exact iff_of_true (fun i => i.elim0) trivial
159+
· have hm_ne : m ≠ 0 := Nat.pos_iff_ne_zero.mp hm
160+
have hm_inv_ne : (m : ℝ≥0∞)⁻¹ ≠ 0 :=
161+
ENNReal.inv_ne_zero.mpr (ENNReal.natCast_ne_top m)
162+
rw [dif_neg hm_ne, Measure.smul_apply, Measure.finsetSum_apply]
163+
simp only [Measure.dirac_apply, Set.indicator, Set.mem_setOf_eq, Pi.one_apply,
164+
smul_eq_mul]
165+
rw [mul_eq_zero]
166+
constructor
167+
· intro hh
168+
right
169+
apply Finset.sum_eq_zero
170+
intro i _
171+
rw [if_neg]
172+
intro hne
173+
exact hne (hh i)
174+
· rintro (h1 | h2)
175+
· exact absurd h1 hm_inv_ne
176+
· intro i
177+
have hi := (Finset.sum_eq_zero_iff.mp h2) i (Finset.mem_univ i)
178+
by_contra hne
179+
rw [if_pos hne] at hi
180+
exact one_ne_zero hi
181+
182+
/-- The empirical 0-1 error equals the empirical miscount divided by the
183+
sample size. -/
184+
theorem empiricalError_eq_div [DecidableEq β]
185+
[MeasurableSpace α] [MeasurableSpace β]
186+
[MeasurableSingletonClass α] [MeasurableSingletonClass β]
187+
{m : ℕ} (hm : 0 < m) (h : α → β) (S : LabeledSample α β m) :
188+
empiricalError h S = (empiricalMiscount h S : ℝ≥0∞) / m := by
189+
have hm_ne : m ≠ 0 := hm.ne'
190+
unfold empiricalError empiricalMeasure error empiricalMiscount
191+
rw [dif_neg hm_ne, Measure.smul_apply, Measure.finsetSum_apply]
192+
simp only [Measure.dirac_apply, Set.indicator, Set.mem_setOf_eq, Pi.one_apply,
193+
smul_eq_mul]
194+
rw [Finset.sum_boole, ← ENNReal.div_eq_inv_mul]
195+
196+
/-! ### Consistent Learners -/
197+
198+
/-- A learner is *consistent* with the concept class `C` if, on every labeled
199+
sample it receives, its output hypothesis lies in the version space of `C` at
200+
that sample — i.e. the output is in `C` and agrees with every observed
201+
labeled pair. -/
202+
def IsConsistent {m : ℕ} (A : Learner α β m) (C : ConceptClass α β) : Prop :=
203+
∀ S : LabeledSample α β m, A S ∈ VersionSpace C S
204+
205+
/-- A consistent learner's output is always in the concept class. -/
206+
theorem IsConsistent.output_mem_conceptClass {m : ℕ} {A : Learner α β m}
207+
{C : ConceptClass α β} (hA : IsConsistent A C) (S : LabeledSample α β m) :
208+
A S ∈ C := (hA S).1
209+
210+
/-- A consistent learner's output agrees with the sample on every observed
211+
point. -/
212+
theorem IsConsistent.output_agrees {m : ℕ} {A : Learner α β m}
213+
{C : ConceptClass α β} (hA : IsConsistent A C) (S : LabeledSample α β m)
214+
(i : Fin m) :
215+
A S (S i).1 = (S i).2 := (hA S).2 i
216+
217+
/-- A consistent learner has zero empirical miscount on every sample. -/
218+
theorem IsConsistent.empiricalMiscount_eq_zero [DecidableEq β]
219+
{m : ℕ} {A : Learner α β m} {C : ConceptClass α β} (hA : IsConsistent A C)
220+
(S : LabeledSample α β m) :
221+
empiricalMiscount (A S) S = 0 :=
222+
(mem_versionSpace_iff_empiricalMiscount_zero.mp (hA S)).2
223+
224+
/-- A consistent learner has zero empirical error on every sample. -/
225+
theorem IsConsistent.empiricalError_eq_zero
226+
[MeasurableSpace α] [MeasurableSpace β]
227+
[MeasurableSingletonClass α] [MeasurableSingletonClass β]
228+
{m : ℕ} {A : Learner α β m} {C : ConceptClass α β}
229+
(hA : IsConsistent A C) (S : LabeledSample α β m) :
230+
empiricalError (A S) S = 0 :=
231+
(mem_versionSpace_iff_empiricalError_zero.mp (hA S)).2
232+
233+
/-! ### Realizable case -/
234+
235+
/-- A labeled sample `S` is *realizable* by concept class `C` if some concept
236+
in `C` labels every sample point correctly. -/
237+
def Realizable {m : ℕ} (C : ConceptClass α β) (S : LabeledSample α β m) : Prop :=
238+
∃ c ∈ C, ∀ i : Fin m, (S i).2 = c (S i).1
239+
240+
/-- *Realizable version-space nonemptiness.* If a target concept `c` lies in
241+
`C` and the sample `S` is labeled by `c` (i.e. every `(S i).2 = c (S i).1`),
242+
then `c` itself lies in the version space `VersionSpace C S`. -/
243+
theorem mem_versionSpace_of_realizable {m : ℕ} {C : ConceptClass α β}
244+
{c : α → β} (hc : c ∈ C) (S : LabeledSample α β m)
245+
(hS : ∀ i : Fin m, (S i).2 = c (S i).1) :
246+
c ∈ VersionSpace C S :=
247+
⟨hc, fun i => (hS i).symm⟩
248+
249+
/-- A realizable sample has nonempty version space. -/
250+
theorem Realizable.versionSpace_nonempty {m : ℕ} {C : ConceptClass α β}
251+
{S : LabeledSample α β m} (h : Realizable C S) :
252+
(VersionSpace C S).Nonempty :=
253+
⟨h.choose, mem_versionSpace_of_realizable h.choose_spec.1 S h.choose_spec.2⟩
254+
255+
/-! ### Probabilistic Realizable -/
256+
257+
/-- Under the pushforward of a probability measure `P` along the graph map
258+
`x ↦ (x, c x)`, the graph of `c` has measure `1`. -/
259+
private lemma map_graph_eq_one
260+
[MeasurableSpace α] [MeasurableSpace β]
261+
{c : α → β} (hcm : Measurable c) (P : Measure α) [IsProbabilityMeasure P]
262+
(hG : MeasurableSet {p : α × β | p.2 = c p.1}) :
263+
(P.map (fun x => (x, c x))) {p : α × β | p.2 = c p.1} = 1 := by
264+
have hφ : Measurable (fun x : α => (x, c x)) := by fun_prop
265+
rw [Measure.map_apply hφ hG]
266+
have hpre : (fun x : α => (x, c x)) ⁻¹' {p : α × β | p.2 = c p.1} = Set.univ := by
267+
ext x; simp
268+
rw [hpre, measure_univ]
269+
270+
/-- The iid product of the realizable joint distribution assigns measure `1`
271+
to the set of samples where every coordinate lies on the graph of `c`. -/
272+
private lemma pi_map_graph_eq_one
273+
[MeasurableSpace α] [MeasurableSpace β]
274+
{c : α → β} (hcm : Measurable c) (P : Measure α) [IsProbabilityMeasure P]
275+
(hG : MeasurableSet {p : α × β | p.2 = c p.1}) {m : ℕ} :
276+
(Measure.pi (fun _ : Fin m => P.map (fun x => (x, c x))))
277+
(Set.univ.pi (fun _ : Fin m => {p : α × β | p.2 = c p.1})) = 1 := by
278+
have hφ : Measurable (fun x : α => (x, c x)) := by fun_prop
279+
haveI : IsProbabilityMeasure (P.map (fun x : α => (x, c x))) :=
280+
Measure.isProbabilityMeasure_map hφ.aemeasurable
281+
rw [Measure.pi_pi]
282+
simp [map_graph_eq_one hcm P hG]
283+
284+
/-- Under iid sampling from the realizable joint distribution induced by
285+
`c ∈ C` and a probability measure `P` on `α`, the target concept `c` lies in
286+
the version space almost surely. -/
287+
theorem ae_mem_versionSpace_of_realizable
288+
[MeasurableSpace α] [MeasurableSpace β]
289+
{C : ConceptClass α β} {c : α → β} (hc : c ∈ C) (hcm : Measurable c)
290+
(hG : MeasurableSet {p : α × β | p.2 = c p.1})
291+
(P : Measure α) [IsProbabilityMeasure P] (m : ℕ) :
292+
∀ᵐ S : LabeledSample α β m
293+
∂(Measure.pi (fun _ : Fin m => P.map (fun x => (x, c x)))),
294+
c ∈ VersionSpace C S := by
295+
have hφ : Measurable (fun x : α => (x, c x)) := by fun_prop
296+
haveI : IsProbabilityMeasure (P.map (fun x : α => (x, c x))) :=
297+
Measure.isProbabilityMeasure_map hφ.aemeasurable
298+
rw [ae_iff]
299+
have hsub : {S : Fin m → α × β | ¬ c ∈ VersionSpace C S} ⊆
300+
(Set.univ.pi (fun _ : Fin m => {p : α × β | p.2 = c p.1}))ᶜ := by
301+
intro S hS hcontra
302+
simp only [Set.mem_pi, Set.mem_univ, true_implies, Set.mem_setOf_eq] at hcontra
303+
exact hS ⟨hc, fun i => (hcontra i).symm⟩
304+
have hcompl : (Measure.pi (fun _ : Fin m => P.map (fun x : α => (x, c x))))
305+
((Set.univ.pi (fun _ : Fin m => {p : α × β | p.2 = c p.1}))ᶜ) = 0 := by
306+
rw [prob_compl_eq_one_sub (MeasurableSet.univ_pi fun _ => hG),
307+
pi_map_graph_eq_one hcm P hG, tsub_self]
308+
exact measure_mono_null hsub hcompl
309+
310+
end Cslib.MachineLearning.PACLearning

‎references.bib‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -382,3 +382,42 @@ @incollection{WinskelNielsen1995
382382
url = {https://doi.org/10.1093/oso/9780198537809.003.0001},
383383
eprint = {https://academic.oup.com/book/0/chapter/421962123/chapter-pdf/52352653/isbn-9780198537809-book-part-1.pdf},
384384
}
385+
386+
@inproceedings{Mitchell1977,
387+
author = {Mitchell, Tom M.},
388+
title = {Version Spaces: A Candidate Elimination Approach to Rule Learning},
389+
booktitle = {Proceedings of the 5th International Joint Conference on Artificial Intelligence},
390+
volume = {1},
391+
pages = {305--310},
392+
year = {1977}
393+
}
394+
395+
@article{Mitchell1982,
396+
author = {Mitchell, Tom M.},
397+
title = {Generalization as Search},
398+
journal = {Artificial Intelligence},
399+
volume = {18},
400+
number = {2},
401+
pages = {203--226},
402+
year = {1982},
403+
doi = {10.1016/0004-3702(82)90040-6}
404+
}
405+
406+
@article{Angluin1980,
407+
author = {Angluin, Dana},
408+
title = {Inductive Inference of Formal Languages from Positive Data},
409+
journal = {Information and Control},
410+
volume = {45},
411+
number = {2},
412+
pages = {117--135},
413+
year = {1980},
414+
doi = {10.1016/S0019-9958(80)90285-5}
415+
}
416+
417+
@book{Mitchell1997,
418+
author = {Mitchell, Tom M.},
419+
title = {Machine Learning},
420+
year = {1997},
421+
publisher = {McGraw-Hill},
422+
isbn = {0070428077}
423+
}

0 commit comments

Comments
 (0)