Lemma 30.6: a binary class with a compression scheme of size k in the realizable case has one of size k for the unrealizable case
ProvedUnderstandingML.compression_realizable_to_agnosticagnostic-learningcompression-schemes
Lemma 30.6. Let be a hypothesis class for binary classification, and assume it has a compression scheme of size in the realizable case. Then, it has a compression scheme of size for the unrealizable case as well.
Preamble
import Definitions.Def_UnderstandingML_Compression open MeasureTheory open scoped InnerProductSpace
Formal statement
namespace UnderstandingML
/-- **Lemma 30.6** (p. 412). Let `H` be a hypothesis class for binary classification, and assume
it has a compression scheme of size `k` in the realizable case. Then it has a compression
scheme of size `k` for the unrealizable case as well. -/
theorem compression_realizable_to_agnostic {X : Type*} (H : Set (X → Bool)) (k : ℕ)
(hH : HasCompressionScheme H k) : HasAgnosticCompressionScheme H k := by sorry
end UnderstandingML
Source
Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §30.1 p. 412, Lemma 30.6 with its proof
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.