∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool)
  [MeasurableConceptClass X C],
  (PACLearnable X C ↔ VCDim X C < ⊤) ∧
    (VCDim X C < ⊤ ↔ ∃ k cs, CompressionSchemeWithInfo.size cs = k) ∧
      (VCDim X C < ⊤ ↔
          ∀ ε > 0,
            ∃ m₀,
              ∀ (D : MeasureTheory.Measure X),
                MeasureTheory.IsProbabilityMeasure D → ∀ m ≥ m₀, RademacherComplexity X C D m < ε) ∧
        (PACLearnable X C →
            ∃ L mf,
              (∀ (ε δ : ℝ),
                  0 < ε →
                    0 < δ →
                      ∀ (D : MeasureTheory.Measure X),
                        MeasureTheory.IsProbabilityMeasure D →
                          ∀ c ∈ C,
                            (MeasureTheory.Measure.pi fun x => D)
                                {xs | D {x | L.learn (fun i => (xs i, c (xs i))) x ≠ c x} ≤ ENNReal.ofReal ε} ≥
                              ENNReal.ofReal (1 - δ)) ∧
                (∀ (ε δ : ℝ), 0 < ε → 0 < δ → SampleComplexity X C ε δ ≤ mf ε δ) ∧
                  ∀ (d : ℕ),
                    VCDim X C = ↑d →
                      ∀ (ε δ : ℝ),
                        0 < ε →
                          ε ≤ 1 / 4 →
                            0 < δ →
                              δ ≤ 1 →
                                δ ≤ 1 / 7 →
                                  1 ≤ d → ⌈(↑d - 1) / 2⌉₊ ≤ SampleComplexity X C ε δ ∧ ⌈(↑d - 1) / 2⌉₊ ≤ mf ε δ) ∧
          (VCDim X C < ⊤ ↔ ∃ d, ∀ (m : ℕ), d ≤ m → GrowthFunction X C m ≤ ∑ i ∈ Finset.range (d + 1), m.choose i)