Moran-Yehudayoff Compression Theorem

Finite VC dimension ↔ compression scheme with finite side information.

Architecture

The forward direction (VCDim < ⊤ → compression) uses the Moran-Yehudayoff construction:

1. A proper finite-support learner (from VC + Sauer-Shelah + probabilistic method)
2. A hypothesis envelope (finite image of the learner on bounded subsamples)
3. An approximate minimax strategy on the agreement game
4. Sparse approximation via VC ε-approximation on agreement tests
5. Majority vote reconstruction with incidence side information

The reverse direction (compression → VCDim < ⊤) is by pigeonhole on the bounded set of (kernel, info) pairs.

No Measure Theory

The forward theorem is pure and combinatorial. It uses FinitePMF, Finset, and finite games — no MeasureTheory.Measure, IsProbabilityMeasure, Measure.dirac, or MeasurableSpace hypotheses.

Helper definitions

noncomputable def pointSupport {X : Type u} {m : ℕ} (S : Fin m → X × Bool) : Finset X

Extract the domain points from a labeled sample.

Equations

• pointSupport S = Finset.image (fun (i : Fin m) => (S i).1) Finset.univ

noncomputable def labeledSampleOfFinset {X : Type u} (c : X → Bool) (Z : Finset X) : Fin Z.card → X × Bool

Build a labeled sample from a Finset of points and a concept.

Equations

• labeledSampleOfFinset c Z i = (↑(Z.equivFin.symm i), c ↑(Z.equivFin.symm i))

def supportError {X : Type u} (Y : Finset X) (q : FinitePMF ↥Y) (h c : X → Bool) : ℝ

Weighted error of hypothesis h vs concept c over a FinitePMF on Y.

Equations

• supportError Y q h c = ∑ y : ↥Y, q.prob y * if h ↑y = c ↑y then 0 else 1

theorem supportAgreement_eq_one_sub_supportError {X : Type u} (Y : Finset X) (q : FinitePMF ↥Y) (h c : X → Bool) : (∑ y : ↥Y, q.prob y * if h ↑y = c ↑y then 1 else 0) = 1 - supportError Y q h c

Weighted agreement = 1 - supportError.

theorem supportError_nonneg {X : Type u} (Y : Finset X) (q : FinitePMF ↥Y) (h c : X → Bool) : 0 ≤ supportError Y q h c

supportError is nonneg.

theorem supportError_le_one {X : Type u} (Y : Finset X) (q : FinitePMF ↥Y) (h c : X → Bool) : supportError Y q h c ≤ 1

supportError is at most 1.

Structure: Proper Finite-Support Learner

structure ProperFiniteSupportLearner (X : Type u) (C : ConceptClass X Bool) : Type u

A proper finite-support learner for a concept class C. This structure captures the existence of a bounded-support ERM with error at most 1/3 for any C-realizable finite distribution. CORRECTED: good_on_support returns Finset X (not Fin k → X).

• sampleBound : ℕ
• learn {m : ℕ} : (Fin m → X × Bool) → X → Bool
• output_mem {m : ℕ} (S : Fin m → X × Bool) : self.learn S ∈ C
• good_on_support (c : X → Bool) : c ∈ C → ∀ (Y : Finset X) (q : FinitePMF ↥Y), ∃ Z ⊆ Y, Z.card ≤ self.sampleBound ∧ supportError Y q (self.learn (labeledSampleOfFinset c Z)) c ≤ 1 / 3

theorem vcdim_finite_imp_proper_finite_support_learner (X : Type u) (C : ConceptClass X Bool) (hCne : Set.Nonempty C) (hC : VCDim X C < ⊤) : ∃ (_L : ProperFiniteSupportLearner X C), True

Finite VC dimension implies existence of a proper finite-support learner. The construction uses ERM + finite_support_vc_approx on the disagreement family.

Hypothesis Envelope

def boundedSubsamples {X : Type u} (Y : Finset X) (s : ℕ) : Finset (Finset X)

Bounded subsamples: all subsets of Y with cardinality ≤ s.

Equations

• boundedSubsamples Y s = {Z ∈ Y.powerset | Z.card ≤ s}

noncomputable def hypothesisEnvelope {X : Type u} {C : ConceptClass X Bool} (L : ProperFiniteSupportLearner X C) (c : X → Bool) (Y : Finset X) : Finset (X → Bool)

The hypothesis envelope: the finite set of all possible learner outputs on bounded subsamples of Y, labeled by concept c.

Equations

• hypothesisEnvelope L c Y = Finset.image (fun (Z : Finset X) => L.learn (labeledSampleOfFinset c Z)) (boundedSubsamples Y L.sampleBound)

theorem hypothesisEnvelope_sub {X : Type u} {C : ConceptClass X Bool} (L : ProperFiniteSupportLearner X C) (c : X → Bool) (Y : Finset X) (h : X → Bool) (hh : h ∈ hypothesisEnvelope L c Y) : h ∈ C

Every hypothesis in the envelope is in C.

Agreement Tests

def agreeTest {X : Type u} (c : X → Bool) (x : X) (HY : Finset (X → Bool)) : ↥HY → Bool

Per-point agreement test: for a fixed point x ∈ Y and concept c, maps hypothesis h to whether h(x) = c(x).

Equations

• agreeTest c x HY h = decide (↑h x = c x)

def agreeTests {X : Type u} (c : X → Bool) (Y : Finset X) (HY : Finset (X → Bool)) : Finset (↥HY → Bool)

The family of agreement tests over all points in Y.

Equations

• agreeTests c Y HY = Finset.image (fun (x : X) => agreeTest c x HY) Y

Roundtrip helpers for the compression proof

noncomputable def encodeWitnessInfo {X : Type u} [DecidableEq X] (kernel : Finset (X × Bool)) (c : X → Bool) (K : ℕ) (W : Finset X) : Finset (Fin K)

Encode a witness set W as the set of kernel positions of the pairs (x, c x). The bound kernel.card ≤ K is fed into the encoding through the if branch, so the result has the same shape as the current compressCore code.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def decodeWitnessXCoords {X : Type u} (Z : Finset (X × Bool)) {K : ℕ} (idxs : Finset (Fin K)) : Finset X

Decode the X-coordinates of a block from kernel positions. This matches the current blockHyp shape.

Equations

• decodeWitnessXCoords Z idxs = idxs.biUnion fun (idx : Fin K) => if h : ↑idx < Z.card then {(↑(Z.equivFin.symm ⟨↑idx, h⟩)).1} else ∅

def decodeWitnessLabel {X : Type u} [DecidableEq X] (Z : Finset (X × Bool)) : X → Bool

Decode labels from the kernel. This is exactly the current MY reconstruction convention in your file.

Equations

• decodeWitnessLabel Z x = decide ((x, true) ∈ Z)

theorem decodeWitnessXCoords_encode_eq {X : Type u} [DecidableEq X] (kernel : Finset (X × Bool)) (c : X → Bool) {K : ℕ} (W : Finset X) (hK : kernel.card ≤ K) (hWker : ∀ x ∈ W, (x, c x) ∈ kernel) : decodeWitnessXCoords kernel (encodeWitnessInfo kernel c K W) = W

If every (x, c x) with x ∈ W lies in kernel, and kernel.card ≤ K, then decoding the encoded witness positions gives back exactly W.

theorem decodeWitnessLabel_eq_on_encoded {X : Type u} [DecidableEq X] (kernel : Finset (X × Bool)) (c : X → Bool) (W : Finset X) (hWker : ∀ x ∈ W, (x, c x) ∈ kernel) (hlabels : ∀ p ∈ kernel, p.2 = c p.1) (x : X) : x ∈ W → decodeWitnessLabel kernel x = c x

On the encoded witness support, the decoded label function agrees with the true label function c, provided every pair in the kernel has the correct second coordinate.

theorem labeledSampleOfFinset_eq_of_eq_on_support {X : Type u} [DecidableEq X] {ℓ₁ ℓ₂ : X → Bool} {Z : Finset X} (hℓ : ∀ x ∈ Z, ℓ₁ x = ℓ₂ x) : labeledSampleOfFinset ℓ₁ Z = labeledSampleOfFinset ℓ₂ Z

If two label functions agree on all points of Z, then the labeled samples they induce on Z.equivFin are equal.

theorem roundtrip_blockHyp_eq_rep {X : Type u} [DecidableEq X] (learn : {m : ℕ} → (Fin m → X × Bool) → X → Bool) (kernel : Finset (X × Bool)) (c : X → Bool) (K : ℕ) (W : Finset X) (h : X → Bool) (hK : kernel.card ≤ K) (hWker : ∀ x ∈ W, (x, c x) ∈ kernel) (hlabels : ∀ p ∈ kernel, p.2 = c p.1) (hrep : learn (labeledSampleOfFinset c W) = h) (x : X) : have info := encodeWitnessInfo kernel c K W; have blockXCoords := decodeWitnessXCoords kernel info; have blockLabel := decodeWitnessLabel kernel; learn (labeledSampleOfFinset blockLabel blockXCoords) x = h x

Generic roundtrip theorem for the hround sorry.

If:

• encodeWitnessInfo is used in compressCore,
• decodeWitnessXCoords and decodeWitnessLabel are used in blockHyp, and
• the kernel contains the witness pairs with the correct labels,

then the decoded block hypothesis is exactly the representative hypothesis.

Moran-Yehudayoff forward construction — universe-fixed closure helpers

@[reducible, inline]

abbrev CompressionSchemeWithInfo0 (X : Type u) (Y : Type) (C : ConceptClass X Y) : Type (max (max u 1) 0)

Fix the hidden Info universe parameter of CompressionSchemeWithInfo to 0. This resolves the universe elaboration obstruction: Fin T → Finset (Fin K) is Type 0, while CompressionSchemeWithInfo X Bool C with X : Type u infers Info : Type u. Pinning to .{u, 0, 0} allows Type 0 Info directly.

Equations

• CompressionSchemeWithInfo0 X Y C = CompressionSchemeWithInfo X Y C

@[reducible, inline]

abbrev IncidenceInfo (T K : ℕ) : Type

Concrete side information for the MY construction: each of the T recovered blocks is represented by the set of kernel positions it uses.

Equations

• IncidenceInfo T K = (Fin T → Finset (Fin K))

@[implicit_reducible]

instance instFintypeIncidenceInfo (T K : ℕ) : Fintype (IncidenceInfo T K)

Equations

• instFintypeIncidenceInfo T K = inferInstance

Forward direction: VCDim < ⊤ → compression with info

theorem vcdim_finite_imp_compression_with_info (X : Type u) (C : ConceptClass X Bool) (hC : VCDim X C < ⊤) : ∃ (k : ℕ) (cs : CompressionSchemeWithInfo0 X Bool C), CompressionSchemeWithInfo.size cs = k

The forward direction of the Moran-Yehudayoff theorem: finite VC dimension implies existence of a compression scheme with finite side information.

The construction:

1. Build a proper finite-support learner L from VC + Sauer-Shelah
2. For sample S: extract c, Y = pointSupport S, HY = hypothesis envelope
3. Apply approximate minimax on the agreement game → distribution p on HY
4. Apply VC ε-approximation on agreement tests → T representative hypotheses
5. Kernel = union of witness subsets for T hypotheses
6. Side info = incidence: which hypothesis's witness contains each kernel point
7. Reconstruct by majority vote over T hypotheses

Reverse direction: compression with info → VCDim < ⊤

theorem compress_with_info_injective_on_labelings {X : Type u} {n : ℕ} {C : ConceptClass X Bool} (cs : CompressionSchemeWithInfo X Bool C) (pts : Fin n → X) (_hpts : Function.Injective pts) (f g : Fin n → Bool) (hf_real : ∃ c ∈ C, ∀ (i : Fin n), c (pts i) = f i) (hg_real : ∃ c ∈ C, ∀ (i : Fin n), c (pts i) = g i) (hfg : (cs.compress fun (i : Fin n) => (pts i, f i)) = cs.compress fun (i : Fin n) => (pts i, g i)) : f = g

Pigeonhole core: if two C-realizable samples over the same points with different labelings produce the same (kernel, info) pair, correctness forces the labelings to agree.

theorem compression_with_info_imp_vcdim_finite (X : Type u) (C : ConceptClass X Bool) (hcomp : ∃ (k : ℕ) (cs : CompressionSchemeWithInfo X Bool C), cs.size = k) : VCDim X C < ⊤

Compression with side info implies finite VC dimension. Proof by pigeonhole: compress is injective on C-realizable labelings (by correctness), but compressed outputs form a bounded set.

Biconditional

theorem fundamental_vc_compression_with_info (X : Type u) (C : ConceptClass X Bool) : VCDim X C < ⊤ ↔ ∃ (k : ℕ) (cs : CompressionSchemeWithInfo0 X Bool C), CompressionSchemeWithInfo.size cs = k