Structured Complexity Measures

Compression schemes, algorithmic stability, multiclass dimensions, real-valued dimensions, teaching/eluder dimensions, SQ dimension, KL complexity, margin theory, covering numbers.

Compression Schemes

structure CompressionScheme (X : Type u) (Y : Type v) (C : ConceptClass X Y) : Type (max u v)

A compression scheme of size k for concept class C (Littlestone-Warmuth 1986). M-DefinitionRepair (Γ₅₉ → Γ₇₃): parameterized by concept class C.

• compress now returns Finset (X × Y) (actual compressed data points), not Finset (Fin m) (indices). This ensures reconstruct depends ONLY on the compressed subset, enabling the pigeonhole argument.
• correct field guarded by C-realizability: reconstructed hypothesis agrees with every sample point WHEN the sample is C-realizable. This matches Littlestone-Warmuth and Moran-Yehudayoff: compression schemes only need to be correct on samples consistent with some concept in C. Γ₇₃ RESOLVED: previous correct quantified over ALL samples (including inconsistent ones), making CompressionScheme X Bool uninhabited for nonempty X. Now guarded by realizability, enabling genuine non-vacuous proofs.

• compress {m : ℕ} : (Fin m → X × Y) → Finset (X × Y)

  Compression: extract ≤ size labeled examples from the sample

• reconstruct : Finset (X × Y) → X → Y

  Reconstruction: produce hypothesis from compressed subset alone

• size : ℕ

  Size of the compressed representation

• compress_small {m : ℕ} (S : Fin m → X × Y) : (self.compress S).card ≤ self.size

  Compressed set is small

• compress_sub {m : ℕ} (S : Fin m → X × Y) : ↑(self.compress S) ⊆ Set.range S

  Compressed set is a subset of the sample

• correct {m : ℕ} (S : Fin m → X × Y) : (∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) → ∀ (i : Fin m), self.reconstruct (self.compress S) (S i).1 = (S i).2

  Correctness: reconstructed hypothesis agrees with every sample point, when the sample is C-realizable (∃ c ∈ C agreeing with all labels)

structure UnlabeledCompression (X : Type u) (Y : Type v) : Type (max u v)

Unlabeled compression: reconstruction uses only input points, not labels.

• size : ℕ
• compress {m : ℕ} : (Fin m → X × Y) → Finset (Fin m)
• reconstruct {m : ℕ} : (Fin m → X) → Finset (Fin m) → Concept X Y
• small {m : ℕ} (S : Fin m → X × Y) : (self.compress S).card ≤ self.size

Algorithmic Stability

structure AlgorithmicStability (X : Type u) (Y : Type v) : Type (max u v)

Algorithmic stability: removing one example changes the loss by at most β.

• learner : BatchLearner X Y

  The learner whose stability we measure

• beta : ℝ

  Stability parameter

• beta_nonneg : 0 ≤ self.beta
• loss : LossFunction Y
• stable {m : ℕ} (S : Fin (m + 1) → X × Y) (i : Fin (m + 1)) (z : X × Y) : |self.loss (self.learner.learn S z.1) z.2 - self.loss (self.learner.learn (fun (j : Fin m) => S (i.succAbove j)) z.1) z.2| ≤ self.beta

  Stability: for any sample S and any index i, the loss of L(S) vs L(S\i) on any fresh point z differs by at most β. S\i denotes the sample with the i-th element removed.

Multiclass and Real-Valued Extensions

noncomputable def NatarajanDim (X : Type u) (Y : Type v) [Fintype Y] (C : ConceptClass X Y) : WithTop ℕ

Natarajan dimension: multiclass generalization of VC dimension. Largest d such that ∃ S with |S| = d and two witness functions f₀ f₁ : S → Y disagreeing everywhere on S, such that for every binary selection h, some concept in C picks f₀ or f₁ at each point according to h.

Equations

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

noncomputable def DSDim (X : Type u) (Y : Type v) [Fintype Y] (C : ConceptClass X Y) : WithTop ℕ

DS dimension: multiclass shattering where EVERY labeling is realizable. Strictly stronger than Natarajan dimension.

Equations

• DSDim X Y C = ⨆ (S : Finset X), ⨆ (_ : ∀ (f : X → Y), ∃ c ∈ C, ∀ x ∈ S, c x = f x), ↑S.card

theorem DSDim_le_NatarajanDim (X : Type u) (Y : Type v) [Fintype Y] [Nontrivial Y] (C : ConceptClass X Y) : DSDim X Y C ≤ NatarajanDim X Y C

DS dimension ≤ Natarajan dimension: DS-shattering (every labeling realizable) is strictly STRONGER than Natarajan-shattering (2-coloring witness), so fewer sets satisfy the DS condition, hence DSDim ≤ NatarajanDim. Requires |Y| ≥ 2 (Nontrivial Y): when |Y| = 1, Natarajan witnesses f₀ ≠ f₁ cannot exist. M-DefinitionRepair (Γ₈): original statement had wrong direction.

noncomputable def Pseudodimension (X : Type u) (C : ConceptClass X ℝ) : WithTop ℕ

Pseudodimension: real-valued generalization of VC dimension. Largest d such that ∃ S with |S| = d and thresholds t, such that for every binary labeling, some concept crosses the thresholds accordingly.

Equations

• Pseudodimension X C = ⨆ (S : Finset X), ⨆ (t : X → ℝ), ⨆ (_ : ∀ (b : X → Bool), ∃ c ∈ C, ∀ x ∈ S, (b x = true → c x ≥ t x) ∧ (b x = false → c x < t x)), ↑S.card

noncomputable def FatShatteringDim (X : Type u) (C : ConceptClass X ℝ) (γ : ℝ) (_hγ : 0 < γ) : WithTop ℕ

Fat-shattering dimension at margin γ > 0. Like pseudodimension but with γ-margin on both sides of the threshold.

Equations

• FatShatteringDim X C γ _hγ = ⨆ (S : Finset X), ⨆ (t : X → ℝ), ⨆ (_ : ∀ (b : X → Bool), ∃ c ∈ C, ∀ x ∈ S, (b x = true → c x ≥ t x + γ) ∧ (b x = false → c x ≤ t x - γ)), ↑S.card

Other Complexity Measures

noncomputable def SQDimension (X : Type u) [MeasurableSpace X] (C : ConceptClass X Bool) (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (τ : ℝ) : WithTop ℕ

SQ dimension: largest d such that there exist d concepts in C with pairwise small correlations under D. Captures the hardness of learning C using only statistical queries (expected values of functions of the sample). M-DefinitionRepair: added distribution parameter D (originally missing).

Equations

• SQDimension X C D τ = ⨆ (S : Finset (Concept X Bool)), ⨆ (_ : ↑S ⊆ C ∧ ∀ c₁ ∈ S, ∀ c₂ ∈ S, c₁ ≠ c₂ → |∫ (x : X), if c₁ x = c₂ x then 1 else -1 ∂D| ≤ τ), ↑S.card

noncomputable def CoveringNumber (X : Type u) (C : ConceptClass X Bool) (d : Concept X Bool → Concept X Bool → ℝ) (ε : ℝ) : ℕ

Covering number: minimum number of balls of radius ε (under metric d) to cover C.

Equations

• CoveringNumber X C d ε = sInf {k : ℕ | ∃ (S : Finset (Concept X Bool)), S.card ≤ k ∧ ∀ c ∈ C, ∃ s ∈ S, d c s ≤ ε}

noncomputable def TeachingDim (X : Type u) (C : ConceptClass X Bool) : WithTop ℕ

Teaching dimension: max over concepts of min teaching set size. A teaching set for c ∈ C is a set of labeled examples consistent with c that distinguishes c from all other concepts in C.

Equations

• TeachingDim X C = ⨆ c ∈ C, ⨅ (T : Finset (X × Bool)), ⨅ (_ : (∀ p ∈ T, c p.1 = p.2) ∧ ∀ c' ∈ C, c' ≠ c → ∃ p ∈ T, c' p.1 ≠ p.2), ↑T.card

noncomputable def EluderDim (X : Type u) (C : ConceptClass X Bool) : WithTop ℕ

Eluder dimension: length of the longest eluder-independent sequence. Each element xᵢ has two concepts in C agreeing on x₁,...,x_{i-1} but disagreeing on xᵢ.

Equations

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

noncomputable def KLComplexity (α : Type u_1) (prior posterior : α → ℝ) : ℝ

KL complexity: KL divergence D_KL(posterior ‖ prior). Uses the convention 0 · log(0/·) = 0 and · · log(·/0) = +∞ (the tsum returns 0 for non-summable families).

Equations

• KLComplexity α prior posterior = ∑' (x : α), if prior x > 0 ∧ posterior x > 0 then posterior x * Real.log (posterior x / prior x) else 0

structure MarginTheory (X : Type u) : Type u

Margin theory: framework connecting margins to generalization.

• margin : ℝ
• margin_pos : 0 < self.margin
• conceptClass : ConceptClass X ℝ
• bound : ℕ → ℝ

Compression with Side Information (Moran-Yehudayoff 2016)

The Moran-Yehudayoff theorem proves compression WITH finite side information. The paper's definition: κ : LC(∞) → LC(k) × I where I is a finite set. CompressionScheme above is strictly stronger (no side information).

structure CompressionSchemeWithInfo (X : Type u) (Y : Type v) (C : ConceptClass X Y) : Type (max (max u (u_1 + 1)) v)

A labeled compression scheme with finite side information. This is the object proved to exist by Moran-Yehudayoff (2016, arXiv:1503.06960).

The current CompressionScheme is strictly stronger: it requires reconstruction from the compressed Finset alone (no side information). See Open_NoInfoCompressionStrengthening for that conjecture.

• Info : Type u_1

  The side information type

• info_finite : Fintype self.Info

  Side information is finite

• compress {m : ℕ} : (Fin m → X × Y) → Finset (X × Y) × self.Info

  Compression: extract ≤ kernelSize labeled examples + side information

• reconstruct : Finset (X × Y) → self.Info → X → Y

  Reconstruction: produce hypothesis from compressed subset AND side information

• kernelSize : ℕ

  Kernel size bound

• compress_small {m : ℕ} (S : Fin m → X × Y) : (self.compress S).1.card ≤ self.kernelSize

  Compressed set is small

• compress_sub {m : ℕ} (S : Fin m → X × Y) : ↑(self.compress S).1 ⊆ Set.range S

  Compressed set is a subset of the sample

• correct {m : ℕ} (S : Fin m → X × Y) : (∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) → ∀ (i : Fin m), self.reconstruct (self.compress S).1 (self.compress S).2 (S i).1 = (S i).2

  Correctness: reconstructed hypothesis agrees with every sample point, when the sample is C-realizable

noncomputable def CompressionSchemeWithInfo.size {X : Type u} {Y : Type v} {C : ConceptClass X Y} (cs : CompressionSchemeWithInfo X Y C) : ℕ

Total size of a compression scheme with side information: kernel size + number of side information states. (The paper uses k + log₂(|I|+1); we use the simpler k + |I| which is an upper bound and avoids importing Real.log.)

Equations

• cs.size = cs.kernelSize + Fintype.card cs.Info

def CompressionScheme.toWithInfo {X : Type u} {Y : Type v} {C : ConceptClass X Y} (cs : CompressionScheme X Y C) : CompressionSchemeWithInfo X Y C

The current CompressionScheme (no side info) embeds into CompressionSchemeWithInfo with trivial side information Info := PUnit.

Equations

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

def Open_NoInfoCompressionStrengthening : Prop

OPEN CONJECTURE: Does finite VC dimension imply compression WITHOUT side information? This is strictly stronger than the Moran-Yehudayoff theorem. The O(d) version is the Littlestone-Warmuth / Floyd-Warmuth conjecture (open since 1986).

Equations

• Open_NoInfoCompressionStrengthening = ∀ (X : Type ?u.8) (C : ConceptClass X Bool), VCDim X C < ⊤ → ∃ (k : ℕ) (cs : CompressionScheme X Bool C), cs.size = k