Finite VC dimension ⟺ PAC learnability. The measure-theoretic half: VCDim X C < ⊤ exactly when C is PAC learnable. This is the kernel's vc_characterization, surfaced for the independent module; it requires the domain's measurability structure.

VC characterization: C is PAC-learnable iff VCDim(C) < ∞.

PROOF DECOMPOSITION: This theorem factors through the two directions above: ← : vcdim_finite_imp_uc + uc_imp_pac (in Generalization.lean) → : pac_imp_vcdim_finite (contrapositive via double-sample)

HC at this joint: The ← direction crosses from combinatorics (VCDim, GrowthFunction) to measure theory (Measure.pi, TrueError). The → direction crosses from measure theory back to combinatorics. Both crossings have HC > 0.

UK₈: The ↔ hides an ASYMMETRY: the ← proof is constructive (produces ERM), while the → proof is non-constructive (produces hard distribution).

Direction ←: finite VCDim implies PAC learnability.

PROOF ROUTE (via new infrastructure in Generalization.lean): Step 1: VCDim < ∞ → HasUniformConvergence (vcdim_finite_imp_uc) Sub-step 1a: Sauer-Shelah gives GrowthFunction bound Sub-step 1b: Symmetrization reduces UC to growth function counting Sub-step 1c: Concentration inequality closes the bound Step 2: HasUniformConvergence → PACLearnable (uc_imp_pac) Sub-step 2a: Construct ERM learner Sub-step 2b: ERM is consistent in realizable case Sub-step 2c: Consistent + UC → low TrueError

KU₁₈: C.Nonempty is needed for ERM but not stated as hypothesis. If C = ∅, then PACLearnable is vacuously true (∀ c ∈ C, ... is vacuous). But ERM needs a fallback hypothesis from C. Is this a genuine gap or does the empty case work out vacuously?

Counterdefinition (COUNTER-4): If the ERM approach fails for computational reasons (ERM is noncomputable, and we need a computable learner for computational learning theory), swap to the compression-based proof: VCDim < ∞ → finite compression scheme (Moran-Yehudayoff 2016) → compression scheme learner is PAC. Swap condition: When proving COMPUTATIONAL PAC learnability (polynomial time).

Finite VCDim implies uniform convergence. Proof: VCDim < ∞ → UC.

• Finite X: direct Hoeffding per-hypothesis + finite union bound.
• Infinite X: Sauer-Shelah → symmetrization + growth function → UC.

UC bad-event bound: for m ≥ m₀(v,ε,δ), the probability of the bad event (∃ h with |TrueErr-EmpErr| ≥ ε) is at most δ. Composes symmetrization_uc_bound with growth_exp_le_delta.

The symmetrization uniform convergence bound: two-sided version. P[∃h∈C: |TrueErr-EmpErr| ≥ ε] ≤ 4·GF(C,2m)·exp(-mε²/8).

Proof strategy (4 steps):

1. Decompose absolute value: |TrueErr - EmpErr| ≥ ε ↔ (TrueErr - EmpErr ≥ ε) ∨ (EmpErr - TrueErr ≥ ε)

2. Upper tail: P[∃h∈C: TrueErr-EmpErr ≥ ε] ≤ 2·GF(C,2m)·exp(-mε²/8)

• Direct application of symmetrization_step + double_sample_pattern_bound.

3. Lower tail: P[∃h∈C: EmpErr-TrueErr ≥ ε] ≤ 2·GF(C,2m)·exp(-mε²/8)

• Apply the symmetric argument: swap roles of S and S' in the double sample.
• Equivalently, apply symmetrization_step to the event EmpErr-TrueErr ≥ ε and bound the double-sample event {EmpErr_S - EmpErr_{S'} ≥ ε/2}.
• The bound is symmetric because D^m ⊗ D^m is symmetric under swapping factors. have swap_symmetry : DoubleSampleMeasure D m {p | ∃ h ∈ C, EmpErr(S) - EmpErr(S') ≥ ε/2} = DoubleSampleMeasure D m {p | ∃ h ∈ C, EmpErr(S') - EmpErr(S) ≥ ε/2} := Measure.prod_swap ...

4. Union bound: P[|gap| ≥ ε] ≤ P[gap ≥ ε] + P[gap ≤ -ε] ≤ 2·GF·exp(...) + 2·GF·exp(...) = 4·GF(C,2m)·exp(-mε²/8)

References: SSBD Theorem 6.7, Kakade-Tewari Lecture 19

Symmetrization step for the lower tail: P[∃h: EmpErr-TrueErr ≥ ε] ≤ 2·P_{double}[∃h: EmpErr_S-EmpErr_{S'} ≥ ε/2].

Mirror of symmetrization_step for the opposite direction. Uses hoeffding_one_sided_upper instead of hoeffding_one_sided.

Symmetrization: the probability of a large gap TrueErr-EmpErr is at most twice the probability of a large gap EmpErr'-EmpErr on the double sample.

Proof strategy (6 steps):

1. Witness selection: For S in the bad event, ∃h* ∈ C with TrueErr(h) - EmpErr_S(h) ≥ ε.

2. Ghost sample mean: E_{S'}[EmpErr_{S'}(h)] = TrueErr(h) ≥ EmpErr_S(h*) + ε.

• Uses: MeasureTheory.integral_pi to compute E[EmpErr] over product measure.
• KEY LEMMA: For fixed h, E_{D^m}[EmpiricalError(h,S)] = TrueErrorReal(h,c,D). This is because EmpErr = (1/m)∑ indicator(x_i), and E[indicator(x_i)] = TrueErrorReal. have expected_emp_err : ∀ h* : Concept X Bool, ∫ xs, EmpiricalError X Bool h* (sample xs) (zeroOneLoss Bool) ∂(Measure.pi (fun _ : Fin m => D)) = TrueErrorReal X h* c D := by ...

3. Hoeffding on ghost sample: P_{S'}[EmpErr_{S'}(h) < TrueErr(h) - ε/2] ≤ exp(-mε²/2).

• Apply hoeffding_one_sided with t = ε/2.
• The hm_large hypothesis ensures exp(-mε²/2) < 1/2: 2·ln2 ≤ mε² ⟹ mε²/2 ≥ ln2 ⟹ exp(-mε²/2) ≤ 1/2. have hoeffding_ghost : ∀ h* ∈ C, Measure.pi (fun _ : Fin m => D) {xs' | EmpiricalError X Bool h* (sample xs') (zeroOneLoss Bool) < TrueErrorReal X h* c D - ε/2} ≤ ENNReal.ofReal (Real.exp (-m * (ε/2)^2 * 2)) := by intro h* _; exact hoeffding_one_sided D h* c m hm (ε/2) (by linarith) (by ...) (by ...)

4. Complementary probability: P_{S'}[EmpErr_{S'}(h) - EmpErr_S(h) ≥ ε/2] ≥ 1/2.

• From step 2: TrueErr(h) ≥ EmpErr_S(h) + ε
• From step 3: P[EmpErr_{S'} ≥ TrueErr - ε/2] ≥ 1/2
• Chain: EmpErr_{S'} ≥ TrueErr - ε/2 ≥ EmpErr_S + ε - ε/2 = EmpErr_S + ε/2

5. Conditional to unconditional: The witness h* from step 1 also witnesses the double-sample event ∃h∈C: EmpErr'-EmpErr ≥ ε/2. So: P_{S'}[double event | S bad] ≥ 1/2.

6. Fubini integration: By Measure.prod_apply and Fubini: P_{S,S'}[double event] = ∫_S P_{S'}[double event | S] ≥ (1/2) · P_S[bad event] ⟹ P_S[bad event] ≤ 2 · P_{S,S'}[double event].

MEASURABILITY CONCERNS:

• {xs | ∃ h ∈ C, ...} is NOT obviously measurable for infinite C. Strategy: decompose via restriction patterns. On any fixed xs, the set of labelings {(h(xs 0), ..., h(xs(m-1))) | h ∈ C} has at most GF(C,m) ≤ 2^m elements. So the ∃h event is a finite union of measurable sets.
• EmpiricalError is a finite sum of measurable functions, hence measurable.
• The product σ-algebra on (Fin m → X) × (Fin m → X) is generated by cylinder sets, and our events are in this σ-algebra.

References: SSBD Lemma 4.5, Kakade-Tewari Lecture 19 Lemma 1

On the double sample, the probability that any hypothesis has EmpErr' - EmpErr ≥ ε/2 is bounded by GF(C,2m) · exp(-mε²/8).

Proof strategy (Approach A — standard exchangeability, 5 steps):

1. EXCHANGEABILITY: Under D^m ⊗ D^m, the 2m draws z₁,...,z_{2m} are iid from D. The joint distribution is invariant under permutations of {1,...,2m}.

Key lemma: P_{D^m⊗D^m}[event(S,S')] = E_z[P_{split}[event | z]] where z = merged sample and the split is uniformly random among all C(2m,m) ways to partition z into two groups of m.

2. CONDITIONING: For fixed merged sample z of 2m points:

• C restricts to at most GF(C,2m) distinct labeling patterns on z (deterministic).
• For each pattern p, define: diff(p, split) = EmpErr_{S'}(p) - EmpErr_S(p) = (1/m) ∑_{i∈S'} a_i - (1/m) ∑_{i∈S} a_i where a_i = 1[pattern(z_i) ≠ c(z_i)] ∈ {0,1}.

3. PER-PATTERN HOEFFDING ON SPLITS: For fixed z and fixed pattern p: Under uniformly random split (S,S') of z into two groups of m: diff(p, split) = (1/m) ∑_{i∈S'} a_i - (1/m) ∑_{i∈S} a_i

This is a function of the random partition. By Hoeffding's inequality for sampling without replacement (Serfling 1974): P_split[diff ≥ ε/2] ≤ exp(-mε²/8)

Alternative derivation: Hoeffding without replacement from Hoeffding with replacement (iid signs) via coupling. The without-replacement bound is actually TIGHTER (variance reduction), but the with-replacement bound suffices.

4. UNION BOUND: P_split[∃ pattern: diff ≥ ε/2 | z] ≤ (number of patterns) · max_pattern P_split[diff ≥ ε/2] ≤ GF(C,2m) · exp(-mε²/8)

5. INTEGRATE: P_{D^m⊗D^m}[event] = E_z[P_split[event|z]] (by step 1) ≤ E_z[GF(C,2m) · exp(-mε²/8)] (by step 4, pointwise) = GF(C,2m) · exp(-mε²/8) (bound is independent of z)

Infrastructure needed:

• Fin.sumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) (available in Mathlib)
• mergeSamples / splitMergedSample (defined above)
• SplitMeasure and ValidSplit (defined above)
• Measure.pi permutation invariance (to be proved or imported)
• Hoeffding for sampling without replacement
• GrowthFunction on 2m points + sauer_shelah_exp_bound from Rademacher.lean

MEASURABILITY CONCERNS:

• The merged sample z ↦ P_split[event|z] must be measurable as a function of z. Since the event is a finite union over patterns, and each pattern's indicator is a measurable function of z (finite evaluation), this follows.
• GrowthFunction X C (2*m) is a natural number (deterministic), no measurability issue.

References: SSBD Theorem 6.7, Hoeffding (1963), Serfling (1974)

The number of distinct restriction patterns of C on any n points is at most GF(C,n). For z : Fin n → X, define patterns(z) = {p : Fin n → Bool | ∃ h ∈ C, ∀ i, p i = (h(z i) ≠ c(z i))}. Then patterns(z).ncard ≤ GrowthFunction X C n by definition of GrowthFunction.

Rademacher MGF bound.

cosh(x) ≤ exp(x²/2). Standard sub-Gaussian bound.

Generic finite exchangeability bound. Given a measure-preserving family of transformations on a probability space, a NullMeasurableSet S, and a pointwise bound on the sum of preimage indicators, conclude ν(S) ≤ B.

Pure combinatorial inequality: ∑_{i=0}^d C(m,i) ≤ (em/d)^d for d ≤ m, d ≥ 1.

Key arithmetic lemma for PAC bound: for t > 0, t^d * exp(-t) ≤ (d+1)!/t. Follows from exp(t) ≥ t^(d+1)/(d+1)! (partial sum of Taylor series).

Trivial bound: GrowthFunction ≤ 2^n for all concept classes. Each restriction to an n-element set yields a function in S → Bool, and there are at most 2^n such functions.

Upper-tail Hoeffding: for iid Bernoulli(p) draws, the empirical average overshoots the mean by ≥ t with probability ≤ exp(-2mt²).

This is the mirror of hoeffding_one_sided (which bounds the lower tail). The proof uses the same sub-Gaussian machinery with Z_i = indicator(x_i) - p (instead of p - indicator(x_i)).

One-sided Hoeffding: for iid Bernoulli(p) draws, the empirical average undershoots the mean by ≥ t with probability ≤ exp(-2mt²).

Proof strategy (3 steps):

1. MGF bound (Hoeffding's lemma): For X ∈ [0,1] with E[X] = p, E[exp(s(X-p))] ≤ exp(s²/8).

• Adapt from cosh_le_exp_sq_half infrastructure in Rademacher.lean.
• Key: convexity of exp on [0,1] gives E[exp(sX)] ≤ p·exp(s) + (1-p)·exp(0), then the s²/8 bound follows from ln(1 + x) ≤ x and Taylor expansion. have mgf_bound : ∀ (s : ℝ), ∫ x, Real.exp (s * (indicator x - p)) ∂D ≤ Real.exp (s^2 / 8) := by ...

2. Product independence: E[exp(s·∑(X_i-p))] = ∏ E[exp(s(X_i-p))] ≤ exp(ms²/8).

• Uses MeasureTheory.Measure.pi independence structure.
• Needs: Measure.pi integral factorization for product of functions.
• MEASURABILITY: fun xs => Real.exp (s * ∑ i, f (xs i)) is measurable (composition of measurable functions). have product_bound : ∀ (s : ℝ), ∫ xs, Real.exp (s * ∑ i, (indicator (xs i) - p)) ∂Measure.pi (fun _ => D) ≤ Real.exp (m * s^2 / 8) := by ...

3. Exponential Markov + optimize: P[∑(X_i-p) ≤ -mt] = P[exp(-s·∑(X_i-p)) ≥ exp(smt)] ≤ exp(-smt + ms²/8). Optimize over s: set s = 4t to get ≤ exp(-2mt²).

• Uses Markov's inequality in ENNReal form.
• CAST ISSUE: Markov gives ENNReal bound, need to convert exp(-2mt²) between ENNReal.ofReal and the measure value. have markov_step : ∀ (s : ℝ) (hs : 0 < s), Measure.pi (fun _ => D) {xs | ∑ i, (indicator (xs i) - p) ≤ -(m : ℝ) * t} ≤ ENNReal.ofReal (Real.exp (-(s * m * t) + m * s^2 / 8)) := by ... have optimize : Real.exp (-(4*t * m * t) + m * (4*t)^2 / 8) = Real.exp (-2 * m * t^2) := by ring_nf

CAST ISSUES to watch:

• m : ℕ needs cast to ℝ in the exponent: (m : ℝ)
• EmpiricalError returns ℝ, TrueErrorReal returns ℝ, good — no ENNReal gap
• The measure value is ENNReal, the bound exp(-2mt²) is ℝ≥0∞ via ENNReal.ofReal

References: SSBD Lemma B.3, Hoeffding (1963)

Uniform convergence implies PAC learnability via ERM. The ERM learner (which exists by ermLearn) achieves PAC learning when uniform convergence holds. This is the second half of vcdim_finite_imp_pac.

Output is in the hypothesis space

Every concept in C is measurable

All concepts X → Bool are measurable (for disagreement sets)

Uniform convergence bad event is NullMeasurableSet

Direction →: PAC learnability implies finite VCDim.

PROOF ROUTE (via double-sample infrastructure in Generalization.lean): Step 1: Contrapositive — assume VCDim = ∞ Step 2: For m = mf(ε,δ), extract S with |S| = 2m shattered by C (uses WithTop.eq_top_iff_forall_ge, same as vcdim_univ_infinite) Step 3: Construct D = uniform on S (Finset.uniformMeasure?) KU₁₉: Mathlib's uniform measure on a finite set — does MeasureTheory.Measure.count / Finset.card give IsProbabilityMeasure? Step 4: Double-sample trick via GhostSample + symmetrization Step 5: Counting argument on restricted labelings

HC at this joint: Step 3 requires constructing a specific probability measure from a combinatorial object (the shattered set). This is a P₁→P₂ crossing. UK₉: The construction of the hard distribution is the only non-constructive step. Can it be made constructive? (Related to derandomization in learning.)

If VCDim = ⊤, then C is not PAC learnable. Proof: for any learner L with sample function mf, pick ε = 1/4, δ = 1/4. Let m = mf(1/4, 1/4). Since VCDim = ⊤, ∃ shattered set S with |S| ≥ 2m. Put D = uniform on S. For random labeling, any m-sample learner has expected error ≥ 1/4 on unseen points. This is the core of pac_imp_vcdim_finite (contrapositive direction).

The uniform measure is a probability measure when X is nonempty and finite.

NFL counting core: for a shattered set T with |T| > 2m, there exists a labeling f₀ : ↥T → Bool and its shattering witness c₀ ∈ C such that the number of samples xs : Fin m → ↥T where the learner achieves low error (≤ |T|/4) is at most half the total number of samples. Proof: double-counting + pigeonhole using per_sample_labeling_bound.

Per-sample labeling bound: for any fixed xs : Fin m → α on a Fintype α with 2m < |α|, and any function output : (α → Bool) → (α → Bool) that only depends on the restriction of f to {xs i}, at most half the labelings f : α → Bool have error(f, output(f)) * 4 ≤ |α|.

Proof: pair each f with flip_unseen(f). The pair has complementary disagreements on unseen points, and |unseen| > |α|/2, so at most one can have low error.

Finite VC dimension ⟺ eventually polynomial growth. The purely combinatorial half of the fundamental theorem: VCDim X C < ⊤ exactly when the growth function is eventually bounded by a polynomial.

Polynomial growth implies finite VC dimension. If GrowthFunction X C m ≤ K · m ^ d for all large m, then VCDim X C < ⊤: an infinite VC dimension produces shattered sets of every size, forcing 2 ^ m ≤ K · m ^ d for arbitrarily large m, which is impossible. The hypothesis is the eventually filter (the ∀ m form is unsatisfiable at m = 0); Sauer-Shelah supplies it for m ≥ d.

An infinite VC dimension forces the growth function to be at least 2 ^ m at every size: it shatters sets of every size, by iSup₂_eq_top and downward closure.

Shattering is closed under restriction of the sample: if C shatters S and T ⊆ S, then C shatters T. Any labelling of T extends to a labelling of S, which is realized.

A shattered sample of size m forces the growth function at m to be at least 2 ^ m.

Each restriction count is at most the growth function at the matching sample size.

A shattered sample realizes every labelling, so its restriction-pattern set is everything.

The exponential-beats-polynomial crux. 2 ^ m ≤ K · m ^ d cannot hold for arbitrarily large m, since m ^ d = o(2 ^ m). Stated with the eventually filter so it is applicable (the ∀ m form is unsatisfiable at m = 0 for d ≥ 1).

Finite VC dimension implies eventual polynomial growth. If VCDim X C < ⊤ then the growth function is eventually bounded by a polynomial K · m ^ d.

VCDim < ⊤ → growth function polynomially bounded by partial binomial sum. Forward direction of fundamental_theorem conjunct 5. Uses Sauer-Shelah: GrowthFunction(m) ≤ ∑_{i≤d} C(m,i) where d = VCDim.