theorem fundamental_theorem (X : Type u) [MeasurableSpace X]
    [MeasurableSingletonClass X]
    (C : ConceptClass X Bool)
    [MeasurableConceptClass X C] :
    (PACLearnable X C (*@$\leftrightarrow$@*) VCDim X C < (*@$\top$@*)) (*@$\wedge$@*)
    ((VCDim X C < (*@$\top$@*)) (*@$\leftrightarrow$@*)
      exists (k : N) (cs : CompressionSchemeWithInfo0 X Bool C), cs.size = k) (*@$\wedge$@*)
    ((VCDim X C < (*@$\top$@*)) (*@$\leftrightarrow$@*)
      forall e > 0, exists m0, forall (D : Measure X),
        IsProbabilityMeasure D ->
        forall m (*@$\geq$@*) m0, RademacherComplexity X C D m < e) (*@$\wedge$@*)
    (PACLearnable X C ->
      exists (L : BatchLearner X Bool) (mf : R -> R -> N),
        -- sample complexity sandwich + lower bound
        ...) (*@$\wedge$@*)
    ((VCDim X C < (*@$\top$@*)) (*@$\leftrightarrow$@*)
      exists (d : N), forall (m : N), d (*@$\leq$@*) m ->
        GrowthFunction X C m (*@$\leq$@*)
          Finset.sum (Finset.range (d + 1)) (Nat.choose m)) :=
  -- Proof: assembles from component theorems
  (*@$\langle$@*)vc_characterization X C,
   fundamental_vc_compression X C,
   (vc_characterization X C).symm.trans (fundamental_rademacher X C),
   pac_sample_complexity_sandwich X C,
   (*@$\langle$@*)vcdim_finite_imp_growth_bounded X C,
    growth_bounded_imp_vcdim_finite X C(*@$\rangle\rangle$@*)