Finite-Support VC Approximation via Symmetrization

For finite H, we embed into H ⊕ ℕ (which is Infinite) and push the FinitePMF forward along Sum.inl. This forces the growth-function path in the symmetrization proof, giving a sample bound depending only on d and ε, not on |H| or |A|.

PMF Bridge

Infinite Envelope: H ⊕ ℕ

Boolean Expectation Bridges

Main Theorem

theorem finite_support_vc_approx (d : ℕ) (ε : ℝ) (hε : 0 < ε) : ∃ (T : ℕ) (hT : 0 < T), ∀ {H : Type u_1} [inst : Fintype H] [inst_1 : DecidableEq H] (A : Finset (H → Bool)), A.boolVCDim ≤ d → ∀ (μ : FinitePMF H), ∃ (hs : Fin T → H), ∀ a ∈ A, |boolTestExpectation μ a - boolTestExpectation (empiricalPMF hT hs) a| ≤ ε

Finite-support distributions uniformly approximate any distribution on a VC class. For a class of VC dimension at most d and any ε > 0, there exists T = T(d, ε) such that every finitely supported distribution μ is within ε (uniformly over the class) of some empirical distribution on T points. A density-style reduction that lets the approximate minimax / MWU machinery, which lives in finite support, apply to general distributions.