The fundamental theorem of statistical learning

I am proving a theorem in Lean 4 and submitting it to Conjectura.

## Problem CX001 — The fundamental theorem of statistical learning

A class of binary classifiers can be learned from finitely many samples exactly when its VC dimension is finite.

## Environment (fixed — do not assume anything newer)

- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`

If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.

## The exact statement I must prove

```lean
theorem solution : ∀ (α : Type) [MeasurableSpace α] (C : ConceptClass α Bool),
    IsPACLearnable C Set.univ ↔ HasFiniteVCDim C := by
  sorry
```

## The file I submit

```lean
import Conjectura.Problems.CX001.Statement

namespace Submission

theorem solution : Conjectura.CX001.goal := by
  sorry

end Submission

```

## The Lean definitions of every term in this problem

These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.

### concept class

A concept class over a domain `α` with labels in `β` is a set of functions `α → β` — the hypotheses a learner is allowed to consider. For binary labels it is equivalently a family of subsets of `α`.

```lean
Conjectura.Learning.ConceptClass
-- unfolds to:
abbrev ConceptClass (α β : Type*) := Set (α → β)
```
Defined in this corpus.

### PAC learnable

A concept class is PAC learnable over a family of distributions when for every accuracy and confidence there is a sample size and an `IsPACLearner` achieving them, uniformly over the family. This is the central definition of statistical learning theory.

```lean
Conjectura.Learning.IsPACLearnable
-- unfolds to:
def IsPACLearnable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (C : ConceptClass α β) (𝒟 : Set (Measure (α × β))) : Prop :=
  ∀ ε δ : ENNReal, 0 < ε → 0 < δ →
    ∃ m : ℕ, ∃ L : Learner α β m, ∀ D ∈ 𝒟, IsPACLearner L D C ε δ
```
Defined in this corpus.

### learner

A learner using `m` examples is a function turning a `LabelledSample` into a hypothesis. Everything in learning theory is a statement about how well the output hypothesis generalises beyond the sample.

```lean
Conjectura.Learning.Learner
-- unfolds to:
abbrev Learner (α β : Type*) (m : ℕ) := LabelledSample α β m → (α → β)
```
Defined in this corpus.

### labelled sample

A labelled sample of size `m` is a finite sequence of `(point, label)` pairs — the training data a learner is given.

```lean
Conjectura.Learning.LabelledSample
-- unfolds to:
abbrev LabelledSample (α β : Type*) (m : ℕ) := Fin m → (α × β)
```
Defined in this corpus.

### probably approximately correct

A learner is probably approximately correct at accuracy `ε` and confidence `δ` when, over the draw of an i.i.d. sample of size `m`, it outputs a hypothesis within `ε` of the best concept in the class with probability at least `1 - δ`.

```lean
Conjectura.Learning.IsPACLearner
-- unfolds to:
def IsPACLearner {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {m : ℕ}
    (L : Learner α β m) (D : Measure (α × β)) (C : ConceptClass α β) (ε δ : ENNReal) : Prop :=
  1 - δ ≤ (Measure.pi fun _ : Fin m => D)
    {S : Fin m → (α × β) | predictionError D (L S) ≤ optimalError D C + ε}
```
Defined in this corpus.

### prediction error

The prediction error (0–1 loss) of a hypothesis `h` under a joint distribution `D` on `α × β`: the probability that `h` disagrees with the label.

```lean
Conjectura.Learning.predictionError
-- unfolds to:
noncomputable def predictionError {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (D : Measure (α × β)) (h : α → β) : ENNReal :=
  D {p : α × β | h p.1 ≠ p.2}
```
Defined in this corpus.

### optimal error

The optimal error of a concept class is the least `predictionError` achievable by any concept in it. In the realisable setting this is zero; in the agnostic setting it is the benchmark a learner must approach.

```lean
Conjectura.Learning.optimalError
-- unfolds to:
noncomputable def optimalError {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (D : Measure (α × β)) (C : ConceptClass α β) : ENNReal :=
  ⨅ c ∈ C, predictionError D c
```
Defined in this corpus.

### finite VC dimension

A class has finite VC dimension when some `n` bounds the size of every set it `Shatters`. By the fundamental theorem of statistical learning this is equivalent to being PAC learnable in the binary agnostic setting.

```lean
Conjectura.Learning.HasFiniteVCDim
-- unfolds to:
def HasFiniteVCDim {α : Type*} (C : ConceptClass α Bool) : Prop :=
  ∃ n : ℕ, ∀ W : Finset α, Shatters C (W : Set α) → W.card ≤ n
```
Defined in this corpus.

### shatters

A binary concept class shatters a set when every one of its subsets is cut out by some concept — the class can realise every possible labelling of those points.

```lean
Conjectura.Learning.Shatters
-- unfolds to:
def Shatters {α : Type*} (C : ConceptClass α Bool) (W : Set α) : Prop :=
  ∀ W' ⊆ W, ∃ c ∈ C, ∀ x ∈ W, (c x = true ↔ x ∈ W')
```
Defined in this corpus.

### MeasurableSpace

structure

```lean
MeasurableSpace
```
Defined in Mathlib.

### Set

abbrev

```lean
Set
```
Defined in Mathlib.

### Measure

def

```lean
Measure
```
Defined in Mathlib.

### ENNReal

def

```lean
ENNReal
```
Defined in Mathlib.

### pi

def

```lean
Measure.pi
```
Defined in Mathlib.

### univ

theorem

```lean
Set.univ
```
Defined in Mathlib.

### Finset

structure

```lean
Finset
```
Defined in Mathlib.

### card

theorem

```lean
W.card
```
Defined in Mathlib.

## Rules — submissions violating these are rejected automatically

1. **Do not change the name or type of `solution`.** It must satisfy the
   statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
   Declaring your own `goal`, or redefining a name it depends on, produces a
   proof of a *different* statement and is rejected. This is the single most
   common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
   axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
   accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
   `Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
   `snake_case` theorem names, `UpperCamelCase` types.

## What I want from you

Here is my argument in informal mathematics:

> [PASTE YOUR PROOF SKETCH HERE]

Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.