theorem pac_not_implies_online :
    exists (X : Type) (_ : MeasurableSpace X) (C : ConceptClass X Bool),
      PACLearnable X C (*@$\wedge$@*) (*@$\neg$@*) OnlineLearnable X Bool C := by
  refine (*@$\langle$@*)N, (*@$\top$@*), thresholdClass, ?_, ?_(*@$\rangle$@*)
  . -- PAC learnable: VCDim = 1 < (*@$\top$@*), via UC route
    exact vcdim_finite_imp_pac_via_uc' N thresholdClass
      vcdim_threshold_finite ...
  . -- (*@$\neg$@*) OnlineLearnable: LittlestoneDim = (*@$\top$@*)
    intro hol
    have hfin := forward_direction N thresholdClass hol
    rw [ldim_threshold_top] at hfin
    exact lt_irrefl _ hfin

theorem online_imp_pac (X : Type u) [MeasurableSpace X]
    (C : ConceptClass X Bool) (hol : OnlineLearnable X Bool C)
    [MeasurableConceptClass X C] :
    PACLearnable X C := by
  obtain (*@$\langle$@*)M, hM(*@$\rangle$@*) := hol
  have hvcdim : VCDim X C < (*@$\top$@*) := by
    calc VCDim X C (*@$\leq$@*) M := vcdim_le_of_mistake_bounded hM
      _ < (*@$\top$@*) := WithTop.coe_lt_top M
  exact vcdim_finite_imp_pac_via_uc' X C hvcdim ...