Problem CX-001 — the fundamental theorem of statistical learning

Conjectura.Problems.CX001.Statement

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Conjectura.Defs.ComputerScience.Learning.HasFiniteVCDim
import Conjectura.Defs.ComputerScience.Learning.PACLearnable
import Mathlib.MeasureTheory.Measure.MeasureSpace

/-! # Problem CX-001 — the fundamental theorem of statistical learning

LOCKED: solvers cannot modify this file.
-/

namespace Conjectura.CX001

open MeasureTheory Conjectura.Learning

/-- A binary concept class is PAC learnable over all distributions exactly when its
VC dimension is finite. The forward direction is the hard half. -/
def goal : Prop :=
  ∀ (α : Type) [MeasurableSpace α] (C : ConceptClass α Bool),
    IsPACLearnable C Set.univ ↔ HasFiniteVCDim C

end Conjectura.CX001